Metamath Proof Explorer

Theorem ltnles

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

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

Proof

Step Hyp Ref Expression
1 lenlts 
 |-  ( ( 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 ) )