proposition: Theorem inbetween_step_any_Mi_odd : forall x k l, inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x (loc_Inexact l) -> (2 * k + 1 = nb_steps)%Z -> inbetween start (start + IZR nb_steps * step) x (loc_Inexact l).
proof: Proof. intros x k l Hx Hk. apply inbetween_step_not_Eq with (1 := Hx). lia. inversion_clear Hx as [|l' _ Hl]. now rewrite (middle_odd _ Hk) in Hl. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop