no goals
s m n step : Nat
⊢ range' s (m + 1) step ++ range' (s + step * (m + 1)) n step = range' s (n + (m + 1)) step
simpa [range', Nat.mul_succ, Nat.add_assoc, Nat.add_comm]
  using range'_append (s + step) m n step