Theorem subscan2d

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

	Ref	Expression
Hypotheses	subscand.1	$$⊢\phi \to A\in \mathrm{No}$$
	subscand.2	$$⊢\phi \to B\in \mathrm{No}$$
	subscand.3	$$⊢\phi \to C\in \mathrm{No}$$
Assertion	subscan2d	$$⊢\phi \to \left(A{-}_{s}C=B{-}_{s}C\leftrightarrow A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		subscand.1	$$⊢\phi \to A\in \mathrm{No}$$
2		subscand.2	$$⊢\phi \to B\in \mathrm{No}$$
3		subscand.3	$$⊢\phi \to C\in \mathrm{No}$$
4	1 3	subsvald	$$⊢\phi \to A{-}_{s}C=A{+}_s{+}_s\left(C\right)$$
5	2 3	subsvald	$$⊢\phi \to B{-}_{s}C=B{+}_s{+}_s\left(C\right)$$
6	4 5	eqeq12d	$$⊢\phi \to \left(A{-}_{s}C=B{-}_{s}C\leftrightarrow A{+}_s{+}_s\left(C\right)=B{+}_s{+}_s\left(C\right)\right)$$
7	3	negscld	$$⊢\phi \to {+}_s\left(C\right)\in \mathrm{No}$$
8	1 2 7	addscan2d	$$⊢\phi \to \left(A{+}_s{+}_s\left(C\right)=B{+}_s{+}_s\left(C\right)\leftrightarrow A=B\right)$$
9	6 8	bitrd	$$⊢\phi \to \left(A{-}_{s}C=B{-}_{s}C\leftrightarrow A=B\right)$$