proposition: Lemma round_round_eq_mid_beta_odd_rna_aux3 : forall (fexp1 fexp2 : Z -> Z), Valid_exp fexp1 -> Valid_exp fexp2 -> forall x, 0 < x -> (fexp2 (mag x) <= fexp1 (mag x))%Z -> (fexp1 (mag x) <= mag x)%Z -> x = midp beta fexp1 x -> round beta fexp1 ZnearestA (round beta fexp2 ZnearestA x) = round beta fexp1 ZnearestA x.
proof: Proof. intros fexp1 fexp2 Vfexp1 Vfexp2 x Px Hf2 Hf1 Xmid. destruct (Zle_or_lt (fexp2 (mag x)) (fexp1 (mag x) - 1)) as [H1|H1]. - now apply round_round_eq_mid_beta_odd_rna_aux1. - assert (H : fexp2 (mag x) = fexp1 (mag x)) by lia. now apply round_round_eq_mid_beta_odd_rna_aux2. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core FTZ Double_rounding)