simp [Order.grlex.elem_sum, Variables.mul]
n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
⊢ Order.grlex.elem_sum (Variables.mul { val := x :: xs, property := p } { val := y :: ys, property := q }) =
    Order.grlex.elem_sum { val := x :: xs, property := p } + Order.grlex.elem_sum { val := y :: ys, property := q }
n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
⊢ foldl (fun x y => x + y) (x + y) (zipWith (fun x y => x + y) xs ys) =
    foldl (fun x y => x + y) x xs + foldl (fun x y => x + y) y ys