Theorem: UInt.neg_neg (Algdata/Classes/UInt.lean)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ - -a + 0 = - -a + (-a + a)
Tactic:
rw [UInt.neg_add_self]
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ - -a + (-a + a) = - -a + -a + a
Tactic:
rw [UInt.add_assoc]
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ - -a + -a + a = 0 + a
Tactic:
rw [UInt.neg_add_self]
State after:
no goals