a.lean

lemma range_core_step : ∀ (n : ℕ) (xs ys : list ℕ),
    range_core n (xs ++ ys) = range_core n xs ++ ys
| 0     xs ys := rfl
| (n+1) xs ys := by rw [range_core, range_core, ←cons_append, range_core_step]

lemma range_step (n : ℕ) : range (n.succ) = range n ++ [n] :=
    have h : range_core n [n] = range_core n (nil ++ [n]), by rw nil_append,
    by rw [range, range, range_core, h, range_core_step]