intros h
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
⊢ Order.lex_impl a b → Order.lex_impl (Variables.mul a c) (Variables.mul b c)
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
h : Order.lex_impl a b
⊢ Order.lex_impl (Variables.mul a c) (Variables.mul b c)