proposition: Theorem inbetween_step_Lo_Mi_Eq_odd : forall x k, inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x loc_Exact -> (2 * k + 1 = nb_steps)%Z -> inbetween start (start + IZR nb_steps * step) x (loc_Inexact Lt).
proof: Proof. intros x k Hx Hk. apply inbetween_step_not_Eq with (1 := Hx). lia. inversion_clear Hx as [Hl|]. rewrite Hl. rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_r. apply Rcompare_Lt. rewrite <- mult_IZR. apply IZR_lt. rewrite <- Hk. apply Zlt_succ. exact Hstep. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop