no goals
step s m n : Nat
h : range' s m step <+ range' s n step
⊢ m ≤ n
simpa only [length_range'] using h.length_le
step s m n : Nat
h : m ≤ n
⊢ range' s m step <+ range' s m step ++ range' (s + step * m) (n - m) step
step s m n : Nat
h : m ≤ n
⊢ range' s m step <+ range' s n step
rw [← Nat.sub_add_cancel h, ← range'_append]
no goals
step s m n : Nat
h : m ≤ n
⊢ range' s m step <+ range' s m step ++ range' (s + step * m) (n - m) step
apply sublist_append_left