a b : Nat
⊢ range (a + b) = range a ++ range' a b
a b : Nat
⊢ range (a + b) = range a ++ map (fun x => a + x) (range b)
rw [← range'_eq_map_range]
no goals
a b : Nat
⊢ range (a + b) = range a ++ range' a b
simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 a b).symm