proposition: Lemma round_round_div_beta_odd_rna_aux : forall fexp1 fexp2 : Z -> Z, Valid_exp fexp1 -> Valid_exp fexp2 -> (forall ex, (fexp2 ex <= fexp1 ex)%Z) -> forall x y, 0 < x -> 0 < y -> generic_format beta fexp1 x -> generic_format beta fexp1 y -> round beta fexp1 ZnearestA (round beta fexp2 ZnearestA (x / y)) = round beta fexp1 ZnearestA (x / y).
proof: Proof. intros fexp1 fexp2 Vfexp1 Vfexp2 Hexp x y Px Py Fx Fy. assert (Pxy : 0 < x / y). { now unfold Rdiv; apply Rmult_lt_0_compat; [|apply Rinv_0_lt_compat]. } specialize (Hexp (mag (x / y))). destruct (Req_dec (x / y) (midp beta fexp1 (x / y))) as [Mid|Nmid]. - now apply round_round_eq_mid_beta_odd_rna_aux4. - now apply neq_midpoint_beta_odd. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core FTZ Double_rounding)