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