proposition: Lemma compare_cmp x y : compare x y = float_comparison_of_Xcomparison (cmp x y).
proof: Proof. now unfold cmp; case compare. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig