Theorem 1sne0s

Description: Surreal zero does not equal surreal one. (Contributed by Scott Fenton, 5-Sep-2025)

	Ref	Expression
Assertion	1sne0s	⊢ 1s ≠ 0s

Proof

Step	Hyp	Ref	Expression
1		0slt1s	⊢ 0s <s 1s
2		sgt0ne0	⊢ ( 0s <s 1s → 1s ≠ 0s )
3	1 2	ax-mp	⊢ 1s ≠ 0s