fact: Definition Fadd_fast_aux1 beta s1 s2 m1 m2 e1 e2 e : ufloat beta := let m1' := match (e1 - e)%Z with | Zpos d => shift beta m1 d | _ => m1 end in match (e - e2)%Z with | Zpos nb => let d := shift beta xH nb in match Z.div_eucl (Zpos m2) (Zpos d) with | (Zpos m2', r) => let pos := adjust_pos r d pos_Eq in Fadd_slow_aux1 beta s1 s2 m1' m2' e pos | (Z0, r) => let pos := adjust_pos r d pos_Eq in Ufloat s1 m1' e pos | _ => Unan end | Z0 => Fadd_slow_aux1 beta s1 s2 m1' m2 e pos_Eq | _ => Unan end.
imports: Coq(Reals Bool ZArith) Flocq(Zaux Raux Div Sqrt) Xreal Basic