rw [Order.grlex] at h_le
n : ℕ
a b c : Variables n order.GrLex
h_le : Order.grlex a b
⊢ let sum₁ := Order.grlex.elem_sum (Variables.mul a c);
  let sum₂ := Order.grlex.elem_sum (Variables.mul b c);
  if sum₁ < sum₂ then True
  else if sum₁ = sum₂ then if Order.lex (Variables.mul a c) (Variables.mul b c) then True else False else False
n : ℕ
a b c : Variables n order.GrLex
h_le :
  let sum₁ := Order.grlex.elem_sum a;
  let sum₂ := Order.grlex.elem_sum b;
  if sum₁ < sum₂ then True else if sum₁ = sum₂ then if Order.lex a b then True else False else False
⊢ let sum₁ := Order.grlex.elem_sum (Variables.mul a c);
  let sum₂ := Order.grlex.elem_sum (Variables.mul b c);
  if sum₁ < sum₂ then True
  else if sum₁ = sum₂ then if Order.lex (Variables.mul a c) (Variables.mul b c) then True else False else False