proposition: Theorem abs_of_bnd_n : forall x : R, forall xi zi : FF, BND x xi -> abs_of_bnd_n_helper xi zi = true -> ABS x zi.
proof: Proof. intros x xi zi Hx Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (Hb,H3). generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Fpos0_correct _ H1). clear H1. intro H1. generalize (Fle2_correct _ _ H2). rewrite Fopp2_correct. clear H2. intro H2. generalize (Fle2_correct _ _ H3). rewrite Fopp2_correct. clear H3. intro H3. split. exact H1. apply IRabs_n with (2 := H2) (3 := H3) (4 := Hx). apply Ropp_le_cancel. rewrite Ropp_0. apply Rle_trans with (1 := H1) (2 := H2). Qed.
imports: Gappa_common Gappa_pred_nzr