s n : Nat
⊢ range.loop (s + 1) (range' (s + 1) n) = range' 0 (n + 1 + s)
s n : Nat
⊢ range.loop (s + 1) (range' (s + 1) n) = range' 0 (n + (s + 1))
rw [← Nat.add_assoc, Nat.add_right_comm n s 1]
no goals
s n : Nat
⊢ range.loop (s + 1) (range' (s + 1) n) = range' 0 (n + 1 + s)
exact range_loop_range' s (n + 1)