fact: Parameter mantissa_sub_correct : forall x y, valid_mantissa x -> valid_mantissa y -> (MtoP y < MtoP x)%positive -> MtoP (mantissa_sub x y) = (MtoP x - MtoP y)%positive /\ valid_mantissa (mantissa_sub x y).
imports: Coq(ZArith Reals) Flocq(Zaux Raux) Basic Generic Generic_proof