step s n : Nat
⊢ range' s (1 + n) step = range' s n step ++ [s + step * n]
step s n : Nat
⊢ range' s (n + 1) step = range' s n step ++ [s + step * n]
rw [Nat.add_comm n 1]
no goals
step s n : Nat
⊢ range' s (1 + n) step = range' s n step ++ [s + step * n]
exact (range'_append s n 1 step).symm