fact: Definition Frem_aux1 beta mx my s e : float beta * ufloat beta := let (q1, r1) := Z.div_eucl (Zpos mx) (Zpos my) in let (q2, r2) := match match my with | xH => false | xO p => match Z.compare r1 (Zpos p) with | Lt => false | Eq => match q1 with | Z0 => false | Zpos (xO _) => false | _ => true end | Gt => true end | xI p => match Z.compare r1 (Zpos p) with | Lt => false | Eq => false | Gt => true end end with | false => (q1, r1) | true => (q1 + 1, r1 - Zpos my)%Z end in (match q2 with | Zpos p => Float s p 0 | Z0 => Fzero | _ => Fnan end, match r2 with | Zpos p => Ufloat s p e pos_Eq | Z0 => Uzero | Zneg p => Ufloat (negb s) p e pos_Eq end).
imports: Coq(Reals Bool ZArith) Flocq(Zaux Raux Div Sqrt) Xreal Basic