proposition: Theorem inbetween_step_Mi_Mi_even : forall x k, inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x loc_Exact -> (2 * k = nb_steps)%Z -> inbetween start (start + IZR nb_steps * step) x (loc_Inexact Eq).
proof: Proof. intros x k Hx Hk. apply inbetween_step_not_Eq with (1 := Hx). lia. apply Rcompare_Eq. inversion_clear Hx as [Hx'|]. rewrite Hx', <- Hk, mult_IZR. field. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop