proposition: Lemma round_round_eq_mid_beta_odd_rna_aux2 : 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. assert (H : round beta fexp2 ZnearestA x = round beta fexp1 ZnearestA x). { unfold round, F2R, scaled_mantissa, cexp; simpl. now rewrite Hf2. } rewrite round_generic. - exact H. - apply valid_rnd_N. - now rewrite H; apply generic_format_round; [|apply valid_rnd_N]. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core FTZ Double_rounding)