intros a b c
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
⊢ ∀ (a b c : Polynomial n ord), (a + b) * c = a * c + b * c
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
a b c : Polynomial n ord
⊢ (a + b) * c = a * c + b * c