proposition: Theorem inbetween_step_Lo_not_Eq : forall x l, inbetween start (start + step) x l -> l <> loc_Exact -> inbetween start (start + IZR nb_steps * step) x (loc_Inexact Lt).
proof: Proof. intros x l Hx Hl. assert (Hx' := inbetween_bounds_not_Eq _ _ _ _ Hx Hl). constructor. split. apply Hx'. apply Rlt_trans with (1 := proj2 Hx'). apply Rplus_lt_compat_l. rewrite <- (Rmult_1_l step) at 1. apply Rmult_lt_compat_r. exact Hstep. now apply IZR_lt. apply Rcompare_Lt. apply Rlt_le_trans with (1 := proj2 Hx'). rewrite middle_range. apply Rcompare_not_Lt_inv. rewrite <- (Rmult_1_l step) at 2. rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l. rewrite Rmult_1_r. apply Rcompare_not_Lt. apply IZR_le. now apply (Zlt_le_succ 1). exact Hstep. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop