proposition: Lemma round_round_lt_mid : 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 fexp1 x -> ((fexp2 (mag x) <= fexp1 (mag x) - 1)%Z -> x < midp fexp1 x - / 2 * ulp beta fexp2 x) -> round_round_eq fexp1 fexp2 choice1 choice2 x.
proof: Proof. intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hf1 Hx Hx'. destruct (Zle_or_lt (fexp1 (mag x)) (fexp2 (mag x))) as [Hf2'|Hf2']. - assert (Hf2'' : (fexp2 (mag x) = fexp1 (mag x) :> Z)%Z) by lia. now apply round_round_lt_mid_same_place. - assert (Hf2'' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z) by lia. generalize (Hx' Hf2''); intro Hx''. now apply round_round_lt_mid_further_place. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ