n m : ℕ
h : n < m
⊢ [n] ++ Ico (succ n) m = n :: Ico (n + 1) m
n m : ℕ
h : n < m
⊢ Ico n m = n :: Ico (n + 1) m
rw [← append_consecutive (Nat.le_succ n) h, succ_singleton]
no goals
n m : ℕ
h : n < m
⊢ [n] ++ Ico (succ n) m = n :: Ico (n + 1) m
rfl