Theorem lesubsd

Description: Swap subtrahends in a surreal inequality. (Contributed by Scott Fenton, 29-Jan-2026)

	Ref	Expression
Hypotheses	lesubsd.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	lesubsd.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	lesubsd.3	⊢ ( 𝜑 → 𝐶 ∈ No )
Assertion	lesubsd	⊢ ( 𝜑 → ( 𝐴 ≤s ( 𝐵 -s 𝐶 ) ↔ 𝐶 ≤s ( 𝐵 -s 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lesubsd.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		lesubsd.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		lesubsd.3	⊢ ( 𝜑 → 𝐶 ∈ No )
4		npcans	⊢ ( ( 𝐵 ∈ No ∧ 𝐴 ∈ No ) → ( ( 𝐵 -s 𝐴 ) +s 𝐴 ) = 𝐵 )
5	2 1 4	syl2anc	⊢ ( 𝜑 → ( ( 𝐵 -s 𝐴 ) +s 𝐴 ) = 𝐵 )
6	2 1	subscld	⊢ ( 𝜑 → ( 𝐵 -s 𝐴 ) ∈ No )
7	1 6	addscomd	⊢ ( 𝜑 → ( 𝐴 +s ( 𝐵 -s 𝐴 ) ) = ( ( 𝐵 -s 𝐴 ) +s 𝐴 ) )
8		npcans	⊢ ( ( 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( ( 𝐵 -s 𝐶 ) +s 𝐶 ) = 𝐵 )
9	2 3 8	syl2anc	⊢ ( 𝜑 → ( ( 𝐵 -s 𝐶 ) +s 𝐶 ) = 𝐵 )
10	5 7 9	3eqtr4rd	⊢ ( 𝜑 → ( ( 𝐵 -s 𝐶 ) +s 𝐶 ) = ( 𝐴 +s ( 𝐵 -s 𝐴 ) ) )
11	10	breq2d	⊢ ( 𝜑 → ( ( 𝐴 +s 𝐶 ) ≤s ( ( 𝐵 -s 𝐶 ) +s 𝐶 ) ↔ ( 𝐴 +s 𝐶 ) ≤s ( 𝐴 +s ( 𝐵 -s 𝐴 ) ) ) )
12	2 3	subscld	⊢ ( 𝜑 → ( 𝐵 -s 𝐶 ) ∈ No )
13	1 12 3	leadds1d	⊢ ( 𝜑 → ( 𝐴 ≤s ( 𝐵 -s 𝐶 ) ↔ ( 𝐴 +s 𝐶 ) ≤s ( ( 𝐵 -s 𝐶 ) +s 𝐶 ) ) )
14	3 6 1	leadds2d	⊢ ( 𝜑 → ( 𝐶 ≤s ( 𝐵 -s 𝐴 ) ↔ ( 𝐴 +s 𝐶 ) ≤s ( 𝐴 +s ( 𝐵 -s 𝐴 ) ) ) )
15	11 13 14	3bitr4d	⊢ ( 𝜑 → ( 𝐴 ≤s ( 𝐵 -s 𝐶 ) ↔ 𝐶 ≤s ( 𝐵 -s 𝐴 ) ) )