fact: Parameter mantissa_sqrt_correct : forall x, valid_mantissa x -> let (q,l) := mantissa_sqrt x in let (s,r) := Z.sqrtrem (Zpos (MtoP x)) in Zpos (MtoP q) = s /\ match l with pos_Eq => r = Z0 | pos_Lo => (0 < r <= s)%Z | pos_Mi => False | pos_Up => (s < r)%Z end /\ valid_mantissa q.
imports: Coq(ZArith Reals) Flocq(Zaux Raux) Basic Generic Generic_proof