Set: pp::colors Set: pp::unicode Using: Nat 0 + 1 Nat::add_assoc : ∀ a b c : ℕ, a + (b + c) = a + b + c using.lean:7:6: error: unknown identifier 'add' Using: Nat 0 + 1 Using: Nat::add as plus using.lean:15:6: error: unknown identifier 'plus_assoc' using.lean:17:6: error: unknown identifier 'add'