proposition: Lemma round_round_div_aux : forall fexp1 fexp2 : Z -> Z, Valid_exp fexp1 -> Valid_exp fexp2 -> forall (choice1 choice2 : Z -> bool), (exists n, (beta = 2 * n :> Z)%Z) -> round_round_div_hyp fexp1 fexp2 -> forall x y, 0 < x -> 0 < y -> generic_format beta fexp1 x -> generic_format beta fexp1 y -> round_round_eq fexp1 fexp2 choice1 choice2 (x / y).
proof: Proof. intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Ebeta Hexp x y Px Py Fx Fy. assert (Pxy : 0 < x / y). { apply Rmult_lt_0_compat; [exact Px|]. now apply Rinv_0_lt_compat. } apply round_round_all_mid_cases. - exact Vfexp1. - exact Vfexp2. - exact Pxy. - apply Hexp. - intros Hf1 Hlxy. exfalso. now apply (round_round_div_aux0 fexp1 fexp2 _ _ choice1 choice2 Hexp x y). - intros Hf1 Hlxy. exfalso. now apply (round_round_div_aux1 fexp1 fexp2 _ _ choice1 choice2 Hexp x y). - intro H. apply round_round_eq_mid_beta_even; try assumption. apply Hexp. - intros Hf1 Hlxy. exfalso. now apply (round_round_div_aux2 fexp1 fexp2 _ _ choice1 choice2 Hexp x y). Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ