Theorem sltnle

Description: Surreal less-than in terms of less-than or equal. (Contributed by Scott Fenton, 8-Dec-2021)

	Ref	Expression
Assertion	sltnle	|- ( ( A e. No /\ B e. No ) -> ( A -. B <_s A ) )

Proof

Step	Hyp	Ref	Expression
1		slenlt	|- ( ( B e. No /\ A e. No ) -> ( B <_s A <-> -. A
2	1	ancoms	|- ( ( A e. No /\ B e. No ) -> ( B <_s A <-> -. A
3	2	con2bid	|- ( ( A e. No /\ B e. No ) -> ( A -. B <_s A ) )