no goals
n✝ n : ℕ
⊢ ofDigits (-1) [n] = List.alternatingSum (List.map (fun n => ↑n) [n])
simp [ofDigits, List.alternatingSum]
n a b : ℕ
t : List ℕ
⊢ ↑a + -1 * (↑b + -1 * List.alternatingSum (List.map (fun n => ↑n) t)) =
    ↑a + -↑b + List.alternatingSum (List.map (fun n => ↑n) t)
n a b : ℕ
t : List ℕ
⊢ ofDigits (-1) (a :: b :: t) = List.alternatingSum (List.map (fun n => ↑n) (a :: b :: t))
simp only [ofDigits, List.alternatingSum, List.map_cons, ofDigits_neg_one t]
no goals
n a b : ℕ
t : List ℕ
⊢ ↑a + -1 * (↑b + -1 * List.alternatingSum (List.map (fun n => ↑n) t)) =
    ↑a + -↑b + List.alternatingSum (List.map (fun n => ↑n) t)
ring