Metamath Proof Explorer


Theorem npcans

Description: Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 4-Feb-2025)

Ref Expression
Assertion npcans A No B No A - s B + s B = A

Proof

Step Hyp Ref Expression
1 subscl A No B No A - s B No
2 simpr A No B No B No
3 1 2 addscomd A No B No A - s B + s B = B + s A - s B
4 pncan3s B No A No B + s A - s B = A
5 4 ancoms A No B No B + s A - s B = A
6 3 5 eqtrd A No B No A - s B + s B = A