no goals
start stop step i : Nat
hstep : 0 < step
⊢ (stop - start + step - 1) / step ≤ i ↔ stop - start + step - 1 < step * i + step
rw [← Nat.lt_succ (n := i), Nat.div_lt_iff_lt_mul hstep, Nat.mul_comm, ← Nat.mul_succ]
no goals
start stop step i : Nat
hstep : 0 < step
⊢ stop - start + step - 1 < step * i + step ↔ stop - start + step - 1 < step * i + 1 + (step - 1)
rw [Nat.add_right_comm, Nat.add_assoc, Nat.sub_add_cancel hstep]
no goals
start stop step i : Nat
hstep : 0 < step
⊢ stop - start + step - 1 < step * i + 1 + (step - 1) ↔ stop ≤ start + step * i
rw [Nat.add_sub_assoc hstep, Nat.add_lt_add_iff_lt_right, Nat.lt_succ,
  Nat.sub_le_iff_le_add']