proposition: Theorem inbetween_step_Lo : forall x k l, inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x l -> (0 < k)%Z -> (2 * k + 1 < nb_steps)%Z -> inbetween start (start + IZR nb_steps * step) x (loc_Inexact Lt).
proof: Proof. intros x k l Hx Hk1 Hk2. apply inbetween_step_not_Eq with (1 := Hx). lia. apply Rcompare_Lt. assert (Hx' := inbetween_bounds _ _ (ordered_steps _) _ _ Hx). apply Rlt_le_trans with (1 := proj2 Hx'). apply Rcompare_not_Lt_inv. rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l. apply Rcompare_not_Lt. rewrite <- mult_IZR. apply IZR_le. lia. exact Hstep. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop