proposition: Lemma mantissa_neg_correct : forall x, valid_mantissa x -> MtoZ (mantissa_neg x) = Zneg (MtoP x).
proof: Proof. intros x (p, H). unfold MtoZ, MtoP. simpl. rewrite H. apply refl_equal. Qed.
imports: Coq(Bool ZArith Reals Psatz) Bignums(BigN BigZ) Flocq(Zaux Raux Digits) Basic Generic Generic_proof Specific_sig