proposition: Lemma round_round_div : 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, y <> 0 -> 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 Nzy Fx Fy. unfold round_round_eq. destruct (Rtotal_order x 0) as [Nx|[Zx|Px]]. - destruct (Rtotal_order y 0) as [Ny|[Zy|Py]]. + rewrite <- (Ropp_involutive x). rewrite <- (Ropp_involutive y). rewrite Ropp_div. unfold Rdiv; rewrite <- Ropp_inv_permute; [|lra]. rewrite Ropp_mult_distr_r_reverse. rewrite Ropp_involutive. fold ((- x) / (- y)). apply Ropp_lt_contravar in Nx. apply Ropp_lt_contravar in Ny. rewrite Ropp_0 in Nx, Ny. apply generic_format_opp in Fx. apply generic_format_opp in Fy. now apply round_round_div_aux. + now exfalso; apply Nzy. + rewrite <- (Ropp_involutive x). rewrite Ropp_div. do 3 rewrite round_N_opp. apply Ropp_eq_compat. apply Ropp_lt_contravar in Nx. rewrite Ropp_0 in Nx. apply generic_format_opp in Fx. now apply round_round_div_aux. - rewrite Zx. unfold Rdiv; rewrite Rmult_0_l. now rewrite round_0; [|apply valid_rnd_N]. - destruct (Rtotal_order y 0) as [Ny|[Zy|Py]]. + rewrite <- (Ropp_involutive y). unfold Rdiv; rewrite <- Ropp_inv_permute; [|lra]. rewrite Ropp_mult_distr_r_reverse. do 3 rewrite round_N_opp. apply Ropp_eq_compat. apply Ropp_lt_contravar in Ny. rewrite Ropp_0 in Ny. apply generic_format_opp in Fy. now apply round_round_div_aux. + now exfalso; apply Nzy. + now apply round_round_div_aux. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ