proposition: Lemma PtoM_correct : forall n, MtoP (PtoM n) = n.
proof: Proof. intros. unfold MtoP, PtoM. rewrite BigN.spec_of_pos. apply refl_equal. Qed.
imports: Coq(Bool ZArith Reals Psatz) Bignums(BigN BigZ) Flocq(Zaux Raux Digits) Basic Generic Generic_proof Specific_sig