fact: Definition Fsqrt_core m1 e1 e := let d1 := Zdigits beta m1 in let m1' := (m1 * Zpower beta (e1 - 2 * e))%Z in let (q, r) := Z.sqrtrem m1' in let l := if Zeq_bool r 0 then loc_Exact else loc_Inexact (if Zle_bool r q then Lt else Gt) in (q, l).
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Digits Generic_fmt Float_prop Bracket