proposition: Lemma mantissa_add_correct : forall x y, valid_mantissa x -> valid_mantissa y -> MtoP (mantissa_add x y) = (MtoP x + MtoP y)%positive /\ valid_mantissa (mantissa_add x y).
proof: Proof. intros x y (px, Hx) (py, Hy). unfold mantissa_add, valid_mantissa, MtoP. rewrite BigN.spec_add. rewrite Hx, Hy. repeat split. now exists (px + py)%positive. Qed.
imports: Coq(Bool ZArith Reals Psatz) Bignums(BigN BigZ) Flocq(Zaux Raux Digits) Basic Generic Generic_proof Specific_sig