Metamath Proof Explorer

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 ) )