calc start
  _ < start + step := Nat.lt_add_of_pos_right hstep
  _ ≤ start + step + step * k := Nat.le_add_right ..
  _ = n := hk.2.symm
case succ
α : Type u
β : Type v
step : Nat
hstep : step > 0
len : Nat
IH : ∀ (start : Nat), Nodup (range' start len step)
start n : Nat
hn : n ∈ range' (start + step) len step
k : Nat
hk : k < len ∧ n = start + step + step * k
⊢ start < n
no goals