proposition: Theorem Bleb_correct : forall f1 f2, is_finite f1 = true -> is_finite f2 = true -> Bleb f1 f2 = Rle_bool (B2R f1) (B2R f2).
proof: Proof. intros f1 f2 F1 F2. generalize (Bcompare_correct _ _ F1 F2). unfold Bleb, SFleb, Bcompare. intros ->. case Rcompare_spec; intro H; case Rle_bool_spec; intro H'; try reflexivity; lra. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative