fact: Definition mantissa_sub_correct := fun x y (_ _ : True) (_ : (MtoP y < MtoP x)%positive) => conj (refl_equal (MtoP x - MtoP y)%positive) I.
imports: Coq(ZArith Reals Psatz Bool) Flocq(Zaux Raux) Basic Generic Generic_proof Specific_sig