Theorem n0subs

Description: Subtraction of non-negative surreal integers. (Contributed by Scott Fenton, 26-May-2025)

	Ref	Expression
Assertion	n0subs	$$⊢\left(M\in {\mathbb{N}}_{\mathrm{0s}}\wedge N\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(M{\le }_{s}N\leftrightarrow N{-}_{s}M\in {\mathbb{N}}_{\mathrm{0s}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		breq2	$$⊢x=0_s\to \left(z{\le }_{s}x\leftrightarrow z{\le }_s{0}_s\right)$$
2		oveq1	$$⊢x=0_s\to x{-}_{s}z=0_s{-}_{s}z$$
3	2	eleq1d	$$⊢x=0_s\to \left(x{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow 0_s{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
4	1 3	imbi12d	$$⊢x=0_s\to \left(\left(z{\le }_{s}x\to x{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \left(z{\le }_s{0}_s\to 0_s{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
5	4	ralbidv	$$⊢x=0_s\to \left(\forall z\in {\mathbb{N}}_{\mathrm{0s}}\left(z{\le }_{s}x\to x{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \forall z\in {\mathbb{N}}_{\mathrm{0s}}\left(z{\le }_s{0}_s\to 0_s{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
6		breq2	$$⊢x=y\to \left(z{\le }_{s}x\leftrightarrow z{\le }_{s}y\right)$$
7		oveq1	$$⊢x=y\to x{-}_{s}z=y{-}_{s}z$$
8	7	eleq1d	$$⊢x=y\to \left(x{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow y{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
9	6 8	imbi12d	$$⊢x=y\to \left(\left(z{\le }_{s}x\to x{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \left(z{\le }_{s}y\to y{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
10	9	ralbidv	$$⊢x=y\to \left(\forall z\in {\mathbb{N}}_{\mathrm{0s}}\left(z{\le }_{s}x\to x{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \forall z\in {\mathbb{N}}_{\mathrm{0s}}\left(z{\le }_{s}y\to y{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
11		breq2	$$⊢x=y{+}_s{1}_s\to \left(z{\le }_{s}x\leftrightarrow z{\le }_s\left(y{+}_s{1}_s\right)\right)$$
12		oveq1	$$⊢x=y{+}_s{1}_s\to x{-}_{s}z=\left(y{+}_s{1}_s\right){-}_{s}z$$
13	12	eleq1d	$$⊢x=y{+}_s{1}_s\to \left(x{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow \left(y{+}_s{1}_s\right){-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
14	11 13	imbi12d	$$⊢x=y{+}_s{1}_s\to \left(\left(z{\le }_{s}x\to x{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \left(z{\le }_s\left(y{+}_s{1}_s\right)\to \left(y{+}_s{1}_s\right){-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
15	14	ralbidv	$$⊢x=y{+}_s{1}_s\to \left(\forall z\in {\mathbb{N}}_{\mathrm{0s}}\left(z{\le }_{s}x\to x{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \forall z\in {\mathbb{N}}_{\mathrm{0s}}\left(z{\le }_s\left(y{+}_s{1}_s\right)\to \left(y{+}_s{1}_s\right){-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
16		breq2	$$⊢x=N\to \left(z{\le }_{s}x\leftrightarrow z{\le }_{s}N\right)$$
17		oveq1	$$⊢x=N\to x{-}_{s}z=N{-}_{s}z$$
18	17	eleq1d	$$⊢x=N\to \left(x{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow N{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
19	16 18	imbi12d	$$⊢x=N\to \left(\left(z{\le }_{s}x\to x{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \left(z{\le }_{s}N\to N{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
20	19	ralbidv	$$⊢x=N\to \left(\forall z\in {\mathbb{N}}_{\mathrm{0s}}\left(z{\le }_{s}x\to x{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \forall z\in {\mathbb{N}}_{\mathrm{0s}}\left(z{\le }_{s}N\to N{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
21		n0sge0	$$⊢z\in {\mathbb{N}}_{\mathrm{0s}}\to 0_s{\le }_{s}z$$
22	21	biantrud	$$⊢z\in {\mathbb{N}}_{\mathrm{0s}}\to \left(z{\le }_s{0}_s\leftrightarrow \left(z{\le }_s{0}_s\wedge 0_s{\le }_{s}z\right)\right)$$
23		n0sno	$$⊢z\in {\mathbb{N}}_{\mathrm{0s}}\to z\in \mathrm{No}$$
24		0sno	$$⊢0_s\in \mathrm{No}$$
25		sletri3	$$⊢\left(z\in \mathrm{No}\wedge 0_s\in \mathrm{No}\right)\to \left(z=0_s\leftrightarrow \left(z{\le }_s{0}_s\wedge 0_s{\le }_{s}z\right)\right)$$
26	23 24 25	sylancl	$$⊢z\in {\mathbb{N}}_{\mathrm{0s}}\to \left(z=0_s\leftrightarrow \left(z{\le }_s{0}_s\wedge 0_s{\le }_{s}z\right)\right)$$
27	22 26	bitr4d	$$⊢z\in {\mathbb{N}}_{\mathrm{0s}}\to \left(z{\le }_s{0}_s\leftrightarrow z=0_s\right)$$
28		oveq2	$$⊢z=0_s\to 0_s{-}_{s}z=0_s{-}_s{0}_s$$
29		subsid	$$⊢0_s\in \mathrm{No}\to 0_s{-}_s{0}_s=0_s$$
30	24 29	ax-mp	$$⊢0_s{-}_s{0}_s=0_s$$
31		0n0s	$$⊢0_s\in {\mathbb{N}}_{\mathrm{0s}}$$
32	30 31	eqeltri	$$⊢0_s{-}_s{0}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
33	28 32	eqeltrdi	$$⊢z=0_s\to 0_s{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}$$
34	27 33	biimtrdi	$$⊢z\in {\mathbb{N}}_{\mathrm{0s}}\to \left(z{\le }_s{0}_s\to 0_s{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
35	34	rgen	$$⊢\forall z\in {\mathbb{N}}_{\mathrm{0s}}\left(z{\le }_s{0}_s\to 0_s{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
36		breq1	$$⊢z=x\to \left(z{\le }_{s}y\leftrightarrow x{\le }_{s}y\right)$$
37		oveq2	$$⊢z=x\to y{-}_{s}z=y{-}_{s}x$$
38	37	eleq1d	$$⊢z=x\to \left(y{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow y{-}_{s}x\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
39	36 38	imbi12d	$$⊢z=x\to \left(\left(z{\le }_{s}y\to y{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \left(x{\le }_{s}y\to y{-}_{s}x\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
40	39	cbvralvw	$$⊢\forall z\in {\mathbb{N}}_{\mathrm{0s}}\left(z{\le }_{s}y\to y{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \forall x\in {\mathbb{N}}_{\mathrm{0s}}\left(x{\le }_{s}y\to y{-}_{s}x\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
41		n0sno	$$⊢y\in {\mathbb{N}}_{\mathrm{0s}}\to y\in \mathrm{No}$$
42		peano2no	$$⊢y\in \mathrm{No}\to y{+}_s{1}_s\in \mathrm{No}$$
43		subsid1	$$⊢y{+}_s{1}_s\in \mathrm{No}\to \left(y{+}_s{1}_s\right){-}_s{0}_s=y{+}_s{1}_s$$
44	41 42 43	3syl	$$⊢y\in {\mathbb{N}}_{\mathrm{0s}}\to \left(y{+}_s{1}_s\right){-}_s{0}_s=y{+}_s{1}_s$$
45		peano2n0s	$$⊢y\in {\mathbb{N}}_{\mathrm{0s}}\to y{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
46	44 45	eqeltrd	$$⊢y\in {\mathbb{N}}_{\mathrm{0s}}\to \left(y{+}_s{1}_s\right){-}_s{0}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
47		oveq2	$$⊢z=0_s\to \left(y{+}_s{1}_s\right){-}_{s}z=\left(y{+}_s{1}_s\right){-}_s{0}_s$$
48	47	eleq1d	$$⊢z=0_s\to \left(\left(y{+}_s{1}_s\right){-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow \left(y{+}_s{1}_s\right){-}_s{0}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
49	46 48	syl5ibrcom	$$⊢y\in {\mathbb{N}}_{\mathrm{0s}}\to \left(z=0_s\to \left(y{+}_s{1}_s\right){-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
50	49	2a1dd	$$⊢y\in {\mathbb{N}}_{\mathrm{0s}}\to \left(z=0_s\to \left(\forall x\in {\mathbb{N}}_{\mathrm{0s}}\left(x{\le }_{s}y\to y{-}_{s}x\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(z{\le }_s\left(y{+}_s{1}_s\right)\to \left(y{+}_s{1}_s\right){-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\right)$$
51	50	adantr	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge z\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(z=0_s\to \left(\forall x\in {\mathbb{N}}_{\mathrm{0s}}\left(x{\le }_{s}y\to y{-}_{s}x\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(z{\le }_s\left(y{+}_s{1}_s\right)\to \left(y{+}_s{1}_s\right){-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\right)$$
52		breq1	$$⊢x=z{-}_s{1}_s\to \left(x{\le }_{s}y\leftrightarrow \left(z{-}_s{1}_s\right){\le }_{s}y\right)$$
53		oveq2	$$⊢x=z{-}_s{1}_s\to y{-}_{s}x=y{-}_s\left(z{-}_s{1}_s\right)$$
54	53	eleq1d	$$⊢x=z{-}_s{1}_s\to \left(y{-}_{s}x\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow y{-}_s\left(z{-}_s{1}_s\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
55	52 54	imbi12d	$$⊢x=z{-}_s{1}_s\to \left(\left(x{\le }_{s}y\to y{-}_{s}x\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \left(\left(z{-}_s{1}_s\right){\le }_{s}y\to y{-}_s\left(z{-}_s{1}_s\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
56	55	rspcv	$$⊢z{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\to \left(\forall x\in {\mathbb{N}}_{\mathrm{0s}}\left(x{\le }_{s}y\to y{-}_{s}x\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(\left(z{-}_s{1}_s\right){\le }_{s}y\to y{-}_s\left(z{-}_s{1}_s\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
57	23	adantl	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge z\in {\mathbb{N}}_{\mathrm{0s}}\right)\to z\in \mathrm{No}$$
58		1sno	$$⊢1_s\in \mathrm{No}$$
59	58	a1i	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge z\in {\mathbb{N}}_{\mathrm{0s}}\right)\to 1_s\in \mathrm{No}$$
60	41	adantr	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge z\in {\mathbb{N}}_{\mathrm{0s}}\right)\to y\in \mathrm{No}$$
61	57 59 60	slesubaddd	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge z\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(\left(z{-}_s{1}_s\right){\le }_{s}y\leftrightarrow z{\le }_s\left(y{+}_s{1}_s\right)\right)$$
62	60 57 59	subsubs2d	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge z\in {\mathbb{N}}_{\mathrm{0s}}\right)\to y{-}_s\left(z{-}_s{1}_s\right)=y{+}_s\left(1_s{-}_{s}z\right)$$
63	60 59 57	addsubsassd	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge z\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(y{+}_s{1}_s\right){-}_{s}z=y{+}_s\left(1_s{-}_{s}z\right)$$
64	62 63	eqtr4d	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge z\in {\mathbb{N}}_{\mathrm{0s}}\right)\to y{-}_s\left(z{-}_s{1}_s\right)=\left(y{+}_s{1}_s\right){-}_{s}z$$
65	64	eleq1d	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge z\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(y{-}_s\left(z{-}_s{1}_s\right)\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow \left(y{+}_s{1}_s\right){-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
66	61 65	imbi12d	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge z\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(\left(\left(z{-}_s{1}_s\right){\le }_{s}y\to y{-}_s\left(z{-}_s{1}_s\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \left(z{\le }_s\left(y{+}_s{1}_s\right)\to \left(y{+}_s{1}_s\right){-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
67	66	biimpd	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge z\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(\left(\left(z{-}_s{1}_s\right){\le }_{s}y\to y{-}_s\left(z{-}_s{1}_s\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(z{\le }_s\left(y{+}_s{1}_s\right)\to \left(y{+}_s{1}_s\right){-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
68	56 67	syl9r	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge z\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(z{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\to \left(\forall x\in {\mathbb{N}}_{\mathrm{0s}}\left(x{\le }_{s}y\to y{-}_{s}x\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(z{\le }_s\left(y{+}_s{1}_s\right)\to \left(y{+}_s{1}_s\right){-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\right)$$
69		n0s0m1	$$⊢z\in {\mathbb{N}}_{\mathrm{0s}}\to \left(z=0_s\vee z{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
70	69	adantl	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge z\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(z=0_s\vee z{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
71	51 68 70	mpjaod	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge z\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(\forall x\in {\mathbb{N}}_{\mathrm{0s}}\left(x{\le }_{s}y\to y{-}_{s}x\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(z{\le }_s\left(y{+}_s{1}_s\right)\to \left(y{+}_s{1}_s\right){-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
72	71	ralrimdva	$$⊢y\in {\mathbb{N}}_{\mathrm{0s}}\to \left(\forall x\in {\mathbb{N}}_{\mathrm{0s}}\left(x{\le }_{s}y\to y{-}_{s}x\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \forall z\in {\mathbb{N}}_{\mathrm{0s}}\left(z{\le }_s\left(y{+}_s{1}_s\right)\to \left(y{+}_s{1}_s\right){-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
73	40 72	biimtrid	$$⊢y\in {\mathbb{N}}_{\mathrm{0s}}\to \left(\forall z\in {\mathbb{N}}_{\mathrm{0s}}\left(z{\le }_{s}y\to y{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \forall z\in {\mathbb{N}}_{\mathrm{0s}}\left(z{\le }_s\left(y{+}_s{1}_s\right)\to \left(y{+}_s{1}_s\right){-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
74	5 10 15 20 35 73	n0sind	$$⊢N\in {\mathbb{N}}_{\mathrm{0s}}\to \forall z\in {\mathbb{N}}_{\mathrm{0s}}\left(z{\le }_{s}N\to N{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
75		breq1	$$⊢z=M\to \left(z{\le }_{s}N\leftrightarrow M{\le }_{s}N\right)$$
76		oveq2	$$⊢z=M\to N{-}_{s}z=N{-}_{s}M$$
77	76	eleq1d	$$⊢z=M\to \left(N{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow N{-}_{s}M\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
78	75 77	imbi12d	$$⊢z=M\to \left(\left(z{\le }_{s}N\to N{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \left(M{\le }_{s}N\to N{-}_{s}M\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
79	78	rspcva	$$⊢\left(M\in {\mathbb{N}}_{\mathrm{0s}}\wedge \forall z\in {\mathbb{N}}_{\mathrm{0s}}\left(z{\le }_{s}N\to N{-}_{s}z\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to \left(M{\le }_{s}N\to N{-}_{s}M\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
80	74 79	sylan2	$$⊢\left(M\in {\mathbb{N}}_{\mathrm{0s}}\wedge N\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(M{\le }_{s}N\to N{-}_{s}M\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
81		n0sge0	$$⊢N{-}_{s}M\in {\mathbb{N}}_{\mathrm{0s}}\to 0_s{\le }_s\left(N{-}_{s}M\right)$$
82		n0sno	$$⊢N\in {\mathbb{N}}_{\mathrm{0s}}\to N\in \mathrm{No}$$
83	82	adantl	$$⊢\left(M\in {\mathbb{N}}_{\mathrm{0s}}\wedge N\in {\mathbb{N}}_{\mathrm{0s}}\right)\to N\in \mathrm{No}$$
84		n0sno	$$⊢M\in {\mathbb{N}}_{\mathrm{0s}}\to M\in \mathrm{No}$$
85	84	adantr	$$⊢\left(M\in {\mathbb{N}}_{\mathrm{0s}}\wedge N\in {\mathbb{N}}_{\mathrm{0s}}\right)\to M\in \mathrm{No}$$
86	83 85	subsge0d	$$⊢\left(M\in {\mathbb{N}}_{\mathrm{0s}}\wedge N\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(0_s{\le }_s\left(N{-}_{s}M\right)\leftrightarrow M{\le }_{s}N\right)$$
87	81 86	imbitrid	$$⊢\left(M\in {\mathbb{N}}_{\mathrm{0s}}\wedge N\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(N{-}_{s}M\in {\mathbb{N}}_{\mathrm{0s}}\to M{\le }_{s}N\right)$$
88	80 87	impbid	$$⊢\left(M\in {\mathbb{N}}_{\mathrm{0s}}\wedge N\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(M{\le }_{s}N\leftrightarrow N{-}_{s}M\in {\mathbb{N}}_{\mathrm{0s}}\right)$$