fact: Definition Fadd_fast_aux2 beta prec s1 s2 m1 m2 e1 e2 := let d1 := count_digits beta m1 in let d2 := count_digits beta m2 in let p1 := (Zpos d1 + e1)%Z in let p2 := (Zpos d2 + e2)%Z in if Zle_bool 2 (Z.abs (p1 - p2)) then let e := Z.min (Z.max e1 e2) (Z.max p1 p2 + Z.neg prec) in if Zlt_bool e1 e then Fadd_fast_aux1 beta s2 s1 m2 m1 e2 e1 e else Fadd_fast_aux1 beta s1 s2 m1 m2 e1 e2 e else Fadd_slow_aux2 beta s1 s2 m1 m2 e1 e2 pos_Eq.
imports: Coq(Reals Bool ZArith) Flocq(Zaux Raux Div Sqrt) Xreal Basic