proposition: Theorem Bcompare_correct : forall f1 f2, is_finite f1 = true -> is_finite f2 = true -> Bcompare f1 f2 = Some (Rcompare (B2R f1) (B2R f2)).
proof: Proof. intros f1 f2 H1 H2. unfold Bcompare. rewrite BinarySingleNaN.Bcompare_correct. now rewrite 2!B2R_B2BSN. now rewrite is_finite_B2BSN. now rewrite is_finite_B2BSN. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN