Theorem npcans

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

	Ref	Expression
Assertion	npcans	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(A{-}_{s}B\right){+}_{s}B=A$$

Proof

Step	Hyp	Ref	Expression
1		subscl	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A{-}_{s}B\in \mathrm{No}$$
2		simpr	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to B\in \mathrm{No}$$
3	1 2	addscomd	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(A{-}_{s}B\right){+}_{s}B=B{+}_s\left(A{-}_{s}B\right)$$
4		pncan3s	$$⊢\left(B\in \mathrm{No}\wedge A\in \mathrm{No}\right)\to B{+}_s\left(A{-}_{s}B\right)=A$$
5	4	ancoms	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to B{+}_s\left(A{-}_{s}B\right)=A$$
6	3 5	eqtrd	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(A{-}_{s}B\right){+}_{s}B=A$$