proposition: Lemma mantissa_mul_correct : forall x y, valid_mantissa x -> valid_mantissa y -> MtoP (mantissa_mul x y) = (MtoP x * MtoP y)%positive /\ valid_mantissa (mantissa_mul x y).
proof: Proof. intros x y (px, Hx) (py, Hy). unfold mantissa_mul, valid_mantissa, MtoP. rewrite BigN.spec_mul. rewrite Hx, Hy. simpl. split. apply refl_equal. exists (px * py)%positive. apply refl_equal. Qed.
imports: Coq(Bool ZArith Reals Psatz) Bignums(BigN BigZ) Flocq(Zaux Raux Digits) Basic Generic Generic_proof Specific_sig