proposition: Theorem Fdiv_correct : forall x y, (0 < F2R x)%R -> (0 < F2R y)%R -> let '(m, e, l) := Fdiv x y in (e <= cexp beta fexp (F2R x / F2R y))%Z /\ inbetween_float beta m e (F2R x / F2R y) l.
proof: Proof. intros [m1 e1] [m2 e2] Hm1 Hm2. apply gt_0_F2R in Hm1. apply gt_0_F2R in Hm2. unfold Fdiv. generalize (mag_div_F2R m1 e1 m2 e2 Hm1 Hm2). set (e := Zminus _ _). set (e' := Z.min (Z.min (fexp e) (fexp (e + 1))) (e1 - e2)). intros [H1 H2]. generalize (Fdiv_core_correct m1 e1 m2 e2 e' Hm1 Hm2). destruct Fdiv_core as [m' l]. apply conj. apply Z.le_trans with (1 := Z.le_min_l _ _). unfold cexp. destruct (Zle_lt_or_eq _ _ H1) as [H|H]. - replace (fexp (mag _ _)) with (fexp (e + 1)). apply Z.le_min_r. clear -H1 H2 H ; apply f_equal ; lia. - replace (fexp (mag _ _)) with (fexp e). apply Z.le_min_l. clear -H1 H2 H ; apply f_equal ; lia. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Generic_fmt Float_prop Digits Bracket