feat(set_theory/game/pgame): sub_self_equiv (#14272)

leanprover-community · May 20, 2022 · d217e1d · d217e1d
1 parent a6b90be
commit d217e1d
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/set_theory/game/pgame.lean b/src/set_theory/game/pgame.lean
@@ -1183,6 +1183,9 @@ theorem zero_le_add_right_neg (x : pgame) : 0 ≤ x + -x :=
 theorem add_right_neg_equiv (x : pgame) : x + -x ≈ 0 :=
 ⟨add_right_neg_le_zero x, zero_le_add_right_neg x⟩
 
+theorem sub_self_equiv : ∀ x, x - x ≈ 0 :=
+add_right_neg_equiv
+
 private lemma add_le_add_right' : ∀ {x y z : pgame} (h : x ≤ y), x + z ≤ y + z
 | (mk xl xr xL xR) (mk yl yr yL yR) (mk zl zr zL zR) :=
 λ h, begin