Theorem addsge01d

Description: A surreal is less-than or equal to itself plus a non-negative surreal. (Contributed by Scott Fenton, 24-Feb-2026)

	Ref	Expression
Hypotheses	addsge01d.1	|- ( ph -> A e. No )
	addsge01d.2	|- ( ph -> B e. No )
Assertion	addsge01d	|- ( ph -> ( 0s <_s B <-> A <_s ( A +s B ) ) )

Proof

Step	Hyp	Ref	Expression
1		addsge01d.1	|- ( ph -> A e. No )
2		addsge01d.2	|- ( ph -> B e. No )
3		0sno	|- 0s e. No
4	3	a1i	|- ( ph -> 0s e. No )
5	4 2 1	sleadd2d	|- ( ph -> ( 0s <_s B <-> ( A +s 0s ) <_s ( A +s B ) ) )
6	1	addsridd	|- ( ph -> ( A +s 0s ) = A )
7	6	breq1d	|- ( ph -> ( ( A +s 0s ) <_s ( A +s B ) <-> A <_s ( A +s B ) ) )
8	5 7	bitrd	|- ( ph -> ( 0s <_s B <-> A <_s ( A +s B ) ) )