refine Pairwise.cons ?_ (IH _)
case succ
α : Type u
β : Type v
step : Nat
hstep : step > 0
len : Nat
IH : ∀ (start : Nat), Nodup (range' start len step)
start : Nat
⊢ Nodup (range' start (Nat.succ len) step)
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'