fact: Parameter 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).
imports: Coq(ZArith Reals) Flocq(Zaux Raux) Basic Generic Generic_proof