proposition: Theorem inbetween_step_Hi_Mi_even : forall x k l, inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x l -> l <> loc_Exact -> (2 * k = nb_steps)%Z -> inbetween start (start + IZR nb_steps * step) x (loc_Inexact Gt).
proof: Proof. intros x k l Hx Hl Hk. apply inbetween_step_not_Eq with (1 := Hx). lia. apply Rcompare_Gt. assert (Hx' := inbetween_bounds_not_Eq _ _ _ _ Hx Hl). apply Rle_lt_trans with (2 := proj1 Hx'). apply Rcompare_not_Lt_inv. rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_r. rewrite <- mult_IZR. apply Rcompare_not_Lt. apply IZR_le. rewrite Hk. apply Z.le_refl. exact Hstep. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop