Theorem: t_add_zero (Diploma/Algebra/PolynomialRing.lean)

State before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
⊢ ∀ (a : Polynomial n ord), a + 0 = a
Tactic:
intros p
State after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
⊢ p + 0 = p

State before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
⊢ p + 0 = p
Tactic:
simp [t_add_comm p, t_zero_add]
State after:
no goals