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