fact: Definition mantissa_sign m := match m with | Zneg p => Mnumber true p | Z0 => Mzero | Zpos p => Mnumber false p end.
imports: Coq(ZArith Reals Psatz Bool) Flocq(Zaux Raux) Basic Generic Generic_proof Specific_sig