y z : PGame
h : y ⧏ z
x : PGame
⊢ y + x ⧏ z + x
y z : PGame
h : y ⧏ z
x : PGame
⊢ x + y ⧏ x + z
rw [lf_congr add_comm_equiv add_comm_equiv]
no goals
y z : PGame
h : y ⧏ z
x : PGame
⊢ y + x ⧏ z + x
apply add_lf_add_right h