Theorem pncan2s

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

	Ref	Expression
Assertion	pncan2s	|- ( ( A e. No /\ B e. No ) -> ( ( A +s B ) -s A ) = B )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( A +s B ) = ( A +s B )
2		addscl	|- ( ( A e. No /\ B e. No ) -> ( A +s B ) e. No )
3		simpl	|- ( ( A e. No /\ B e. No ) -> A e. No )
4		simpr	|- ( ( A e. No /\ B e. No ) -> B e. No )
5	2 3 4	subaddsd	|- ( ( A e. No /\ B e. No ) -> ( ( ( A +s B ) -s A ) = B <-> ( A +s B ) = ( A +s B ) ) )
6	1 5	mpbiri	|- ( ( A e. No /\ B e. No ) -> ( ( A +s B ) -s A ) = B )