proposition: Theorem bnd_of_abs : forall x : R, forall xi zi : FF, ABS x xi -> bnd_of_abs_helper xi zi = true -> BND x zi.
proof: Proof. intros x xi zi Hx Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Fle2_correct _ _ H1). rewrite Fopp2_correct. fold float2R. clear H1. intro H1. generalize (Fle2_correct _ _ H2). clear H2. intro H2. assert (H : (-(upper xi) <= x <= (upper xi))%R). apply (Rabs_def2b _ _ (proj2 (proj2 Hx))). split. apply Rle_trans with (1 := H1) (2 := proj1 H). apply Rle_trans with (1 := proj2 H) (2 := H2). Qed.
imports: Gappa_common Gappa_pred_nzr