have rl_mul := t_mul_comm (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
rl_mul : (a + b) * c = c * (a + b)
⊢ (a + b) * c = a * c + b * c