proposition: Lemma mag_div_F2R : forall m1 e1 m2 e2, (0 < m1)%Z -> (0 < m2)%Z -> let e := ((Zdigits beta m1 + e1) - (Zdigits beta m2 + e2))%Z in (e <= mag beta (F2R (Float beta m1 e1) / F2R (Float beta m2 e2)) <= e + 1)%Z.
proof: Proof. intros m1 e1 m2 e2 Hm1 Hm2. rewrite <- (mag_F2R_Zdigits beta m1 e1) by now apply Zgt_not_eq. rewrite <- (mag_F2R_Zdigits beta m2 e2) by now apply Zgt_not_eq. apply mag_div. now apply F2R_neq_0, Zgt_not_eq. now apply F2R_neq_0, Zgt_not_eq. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Generic_fmt Float_prop Digits Bracket