intros a b
n : ℕ
⊢ ∀ (a b : Variables n order.GrLex),
    Order.grlex.elem_sum (Variables.mul a b) = Order.grlex.elem_sum a + Order.grlex.elem_sum b
n : ℕ
a b : Variables n order.GrLex
⊢ Order.grlex.elem_sum (Variables.mul a b) = Order.grlex.elem_sum a + Order.grlex.elem_sum b