proposition: Lemma ordered_steps : forall k, (start + IZR k * step < start + IZR (k + 1) * step)%R.
proof: Proof. intros k. apply Rplus_lt_compat_l. apply Rmult_lt_compat_r. exact Hstep. apply IZR_lt. apply Zlt_succ. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop