proposition: Theorem eql_of_cst : forall x y : R, forall xi yi : FF, BND x xi -> BND y yi -> eql_of_cst_helper xi yi = true -> x = y.
proof: Proof. intros x y xi yi Hx Hy Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Feq2_correct _ _ H1). clear H1. intro H1. generalize (Feq2_correct _ _ H2). clear H2. intro H2. apply Rle_antisym. apply Rle_trans with (1 := proj2 Hx). rewrite H2. apply Hy. apply Rle_trans with (1 := proj2 Hy). rewrite <- H1. apply Hx. Qed.
imports: Gappa_common Gappa_decimal