fact: Parameter mantissa_shr_correct : forall x y z k, valid_mantissa y -> EtoZ z = Zpos x -> (Zpos (shift radix 1 x) <= Zpos (MtoP y))%Z -> let (sq,l) := mantissa_shr y z k in let (q,r) := Z.div_eucl (Zpos (MtoP y)) (Zpos (shift radix 1 x)) in Zpos (MtoP sq) = q /\ l = adjust_pos r (shift radix 1 x) k /\ valid_mantissa sq.
imports: Coq(ZArith Reals) Flocq(Zaux Raux) Basic Generic Generic_proof