no goals
ι : Type ?u.450121
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n : ℕ
x : α
xs : List α
⊢ enumFrom n (x :: xs) = (n, x) :: map (Prod.map succ id) (enumFrom n xs)
rw [enumFrom_cons, add_comm, ← map_fst_add_enumFrom_eq_enumFrom]