proposition: Lemma mantissa_cmp_correct : forall x y, valid_mantissa x -> valid_mantissa y -> mantissa_cmp x y = Z.compare (Zpos (MtoP x)) (Zpos (MtoP y)).
proof: Proof. intros x y (px, Hx) (py, Hy). unfold mantissa_cmp, MtoP. rewrite Hx, Hy, <- Hx, <- Hy. apply BigN.spec_compare. Qed.
imports: Coq(Bool ZArith Reals Psatz) Bignums(BigN BigZ) Flocq(Zaux Raux Digits) Basic Generic Generic_proof Specific_sig