n : Nat
⊢ 0 :: map (fun x => 1 + x) (range' 0 n) = 0 :: map succ (range' 0 n)
n : Nat
⊢ range (n + 1) = 0 :: map succ (range n)
rw [range_eq_range', range_eq_range', range', Nat.add_comm, ← map_add_range']
case e_tail.e_f
n : Nat
⊢ (fun x => 1 + x) = succ
n : Nat
⊢ 0 :: map (fun x => 1 + x) (range' 0 n) = 0 :: map succ (range' 0 n)
congr
no goals
case e_tail.e_f
n : Nat
⊢ (fun x => 1 + x) = succ
exact funext one_add