proposition: Lemma inbetween_step_not_Eq : forall x k l l', inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x l -> (0 < k < nb_steps)%Z -> Rcompare x (start + (IZR nb_steps / 2 * step))%R = l' -> inbetween start (start + IZR nb_steps * step) x (loc_Inexact l').
proof: Proof. intros x k l l' Hx Hk Hl'. constructor. assert (Hx' := inbetween_bounds _ _ (ordered_steps _) _ _ Hx). split. apply Rlt_le_trans with (2 := proj1 Hx'). rewrite <- (Rplus_0_r start) at 1. apply Rplus_lt_compat_l. apply Rmult_lt_0_compat. now apply IZR_lt. exact Hstep. apply Rlt_le_trans with (1 := proj2 Hx'). apply Rplus_le_compat_l. apply Rmult_le_compat_r. now apply Rlt_le. apply IZR_le. lia. now rewrite middle_range. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop