intro n hn
case succ
α : Type u
β : Type v
step : Nat
hstep : step > 0
len : Nat
IH : ∀ (start : Nat), Nodup (range' start len step)
start : Nat
⊢ ∀ (a' : Nat), a' ∈ range' (start + step) len step → start ≠ a'
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
⊢ start ≠ n