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