proposition: Lemma neq_midpoint_beta_odd_aux3 : forall (fexp1 fexp2 : Z -> Z), Valid_exp fexp1 -> Valid_exp fexp2 -> forall (choice1 choice2 : Z -> bool), forall x, 0 < x -> (fexp2 (mag x) <= fexp1 (mag x))%Z -> (fexp1 (mag x) <= mag x)%Z -> x <> midp beta fexp1 x -> round_round_eq beta fexp1 fexp2 choice1 choice2 x.
proof: Proof. intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hf1 Hx. destruct (generic_format_EM beta fexp2 x) as [F2x|NF2x]. { unfold round_round_eq. now rewrite (round_generic _ fexp2); [|apply valid_rnd_N|]. } assert (NF1x : ~ generic_format beta fexp1 x). { now intro H; apply NF2x, (generic_inclusion_mag _ fexp1). } destruct (Rle_or_lt x (midp beta fexp1 x)) as [H1|H1]. - assert (H1' : x < midp beta fexp1 x) by lra. destruct (Rlt_or_le x (midp beta fexp1 x - / 2 * ulp beta fexp2 x)) as [H2|H2]. + now apply round_round_lt_mid. + now apply neq_midpoint_beta_odd_aux1; [| | | |split]. - assert (Hm : midp' beta fexp1 x = midp beta fexp1 x). { now unfold midp', midp; rewrite round_UP_DN_ulp; [field|]. } destruct (Zle_or_lt (fexp1 (mag x)) (fexp2 (mag x))) as [H3|H3]. + assert (H3' : fexp2 (mag x) = fexp1 (mag x)); [now apply Zle_antisym|]. now apply round_round_gt_mid_same_place; [| | |rewrite Hm]. + destruct (Rlt_or_le (midp beta fexp1 x + / 2 * ulp beta fexp2 x) x) as [H2|H2]. * now apply round_round_gt_mid_further_place; [| | |lia| |rewrite Hm]. * now apply neq_midpoint_beta_odd_aux2; [| | | |split]. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core FTZ Double_rounding)