induction len generalizing start with
| zero => exact .nil
| succ len IH =>
  refine Pairwise.cons ?_ (IH _)
  intro n hn; let ⟨k,hk⟩ := mem_range'.mp hn
  suffices start < n from Nat.ne_of_lt this
  calc start
    _ < start + step := Nat.lt_add_of_pos_right hstep
    _ ≤ start + step + step * k := Nat.le_add_right ..
    _ = n := hk.2.symm
α : Type u
β : Type v
start len step : Nat
hstep : step > 0
⊢ Nodup (range' start len step)
no goals