proposition: Lemma mantissa_one_correct : MtoP mantissa_one = xH /\ valid_mantissa mantissa_one.
proof: Proof. repeat split. now exists xH. Qed.
imports: Coq(Bool ZArith Reals Psatz) Bignums(BigN BigZ) Flocq(Zaux Raux Digits) Basic Generic Generic_proof Specific_sig