1	import Base
2	
3	# Facts about Bool and Nat used by the other proof files. Every variable is
4	# reusable (+), so the lemmas can be used inside each other's proofs. Some are
5	# copied from ../framebender/proof_base.bend (same author, MIT).
6	
7	# Bool
8	# ====
9	
10	def Bool.disc_ft(b: Bool) -> Type:
11	  match b:
12	    case False{}:
13	      Unit
14	    case True{}:
15	      Empty
16	
17	law false_ne_true:
18	  for e: {False{} == True{} : Bool}
19	  Empty
20	
21	def false_ne_true(e):
22	  %e : Bool.disc_ft(_)
23	  Unit{}
24	
25	law true_ne_false:
26	  for e: {True{} == False{} : Bool}
27	  Empty
28	
29	def true_ne_false(e):
30	  false_ne_true(Equal.sym(Bool, True{}, False{}, e))
31	
32	law and_true_r_id:
33	  for +a: Bool
34	  {Bool.and(a, True{}) == a : Bool}
35	
36	def and_true_r_id(a):
37	  match a:
38	    case True{}:
39	      {==}
40	    case False{}:
41	      {==}
42	
43	law and_false_r:
44	  for +a: Bool
45	  {Bool.and(a, False{}) == False{} : Bool}
46	
47	def and_false_r(a):
48	  match a:
49	    case True{}:
50	      {==}
51	    case False{}:
52	      {==}
53	
54	law or_false_r:
55	  for +a: Bool
56	  {Bool.or(a, False{}) == a : Bool}
57	
58	def or_false_r(a):
59	  match a:
60	    case True{}:
61	      {==}
62	    case False{}:
63	      {==}
64	
65	law and_true_l:
66	  for +a: Bool
67	  for +b: Bool
68	  for e: {Bool.and(a, b) == True{} : Bool}
69	  {a == True{} : Bool}
70	
71	def and_true_l(a, b, e):
72	  match a:
73	    case True{}:
74	      {==}
75	    case False{}:
76	      Empty.absurd({False{} == True{} : Bool}, false_ne_true(e))
77	
78	law and_true_r:
79	  for +a: Bool
80	  for +b: Bool
81	  for e: {Bool.and(a, b) == True{} : Bool}
82	  {b == True{} : Bool}
83	
84	def and_true_r(a, b, e):
85	  match a:
86	    case True{}:
87	      e
88	    case False{}:
89	      Empty.absurd({b == True{} : Bool}, false_ne_true(e))
90	
91	# A Bool as a number: 0 or 1.
92	def bn(b: Bool) -> Nat:
93	  match b:
94	    case False{}:
95	      0n
96	    case True{}:
97	      1n
98	
99	# Nat: equality
100	# =============
101	
102	def Nat.disc_z(n: Nat) -> Type:
103	  match n:
104	    case 0n:
105	      Empty
106	    case 1n+p:
107	      Unit
108	
109	law succ_ne_zero:
110	  for -n: Nat
111	  for e: {1n+n == 0n : Nat}
112	  Empty
113	
114	def succ_ne_zero(n, e):
115	  %e : Nat.disc_z(_)
116	  Unit{}
117	
118	law zero_ne_succ:
119	  for -n: Nat
120	  for e: {0n == 1n+n : Nat}
121	  Empty
122	
123	def zero_ne_succ(n, e):
124	  succ_ne_zero(n, Equal.sym(Nat, 0n, 1n+n, e))
125	
126	def pred(n: Nat) -> Nat:
127	  match n:
128	    case 0n:
129	      0n
130	    case 1n+p:
131	      p
132	
133	law succ_inj:
134	  for +a: Nat
135	  for +b: Nat
136	  for e: {1n+a == 1n+b : Nat}
137	  {a == b : Nat}
138	
139	def succ_inj(a, b, e):
140	  Equal.cong(Nat, Nat, n => pred(n), 1n+a, 1n+b, e)
141	
142	law eq_refl:
143	  for +n: Nat
144	  {Nat.is_eq(n, n) == True{} : Bool}
145	
146	def eq_refl(n):
147	  match n:
148	    case 0n:
149	      {==}
150	    case 1n+p:
151	      eq_refl(p)
152	
153	law cmp_refl:
154	  for +n: Nat
155	  {Nat.cmp(n, n) == EQ{} : Cmp}
156	
157	def cmp_refl(n):
158	  match n:
159	    case 0n:
160	      {==}
161	    case 1n+p:
162	      cmp_refl(p)
163	
164	law eq_sound:
165	  for +a: Nat
166	  for +b: Nat
167	  for e: {Nat.is_eq(a, b) == True{} : Bool}
168	  {a == b : Nat}
169	
170	def eq_sound(a, b, e):
171	  match a b:
172	    case 0n 0n:
173	      {==}
174	    case 0n 1n+q:
175	      Empty.absurd({0n == 1n+q : Nat}, false_ne_true(e))
176	    case 1n+p 0n:
177	      Empty.absurd({1n+p == 0n : Nat}, false_ne_true(e))
178	    case 1n+p 1n+q:
179	      %eq_sound(p, q, e) : {1n+p == 1n+_ : Nat}
180	      {==}
181	
182	# Nat: addition
183	# =============
184	
185	law add_zero:
186	  for +n: Nat
187	  {Nat.add(n, 0n) == n : Nat}
188	
189	def add_zero(n):
190	  match n:
191	    case 0n:
192	      {==}
193	    case 1n+p:
194	      %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
195	      {==}
196	
197	law add_succ:
198	  for +a: Nat
199	  for +b: Nat
200	  {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}
201	
202	def add_succ(a, b):
203	  match a:
204	    case 0n:
205	      {==}
206	    case 1n+p:
207	      %add_succ(p, b) : {1n+Nat.add(p, 1n+b) == 1n+_ : Nat}
208	      {==}
209	
210	law add_one:
211	  for +n: Nat
212	  {Nat.add(n, 1n) == 1n+n : Nat}
213	
214	def add_one(n):
215	  %add_zero(n) : {Nat.add(n, 1n) == 1n+_ : Nat}
216	  add_succ(n, 0n)
217	
218	law add_comm:
219	  for +a: Nat
220	  for +b: Nat
221	  {Nat.add(a, b) == Nat.add(b, a) : Nat}
222	
223	def add_comm(a, b):
224	  match a:
225	    case 0n:
226	      Equal.sym(Nat, Nat.add(b, 0n), b, add_zero(b))
227	    case 1n+p:
228	      %Equal.sym(Nat, Nat.add(p, b), Nat.add(b, p), add_comm(p, b)) :
229	        {1n+_ == Nat.add(b, 1n+p) : Nat}
230	      Equal.sym(Nat, Nat.add(b, 1n+p), 1n+Nat.add(b, p), add_succ(b, p))
231	
232	law add_assoc:
233	  for +a: Nat
234	  for +b: Nat
235	  for +c: Nat
236	  {Nat.add(Nat.add(a, b), c) == Nat.add(a, Nat.add(b, c)) : Nat}
237	
238	def add_assoc(a, b, c):
239	  match a:
240	    case 0n:
241	      {==}
242	    case 1n+p:
243	      %add_assoc(p, b, c) : {1n+Nat.add(Nat.add(p, b), c) == 1n+_ : Nat}
244	      {==}
245	
246	law add_left_comm:
247	  for +a: Nat
248	  for +b: Nat
249	  for +c: Nat
250	  {Nat.add(a, Nat.add(b, c)) == Nat.add(b, Nat.add(a, c)) : Nat}
251	
252	def add_left_comm(a, b, c):
253	  %add_assoc(a, b, c) : {_ == Nat.add(b, Nat.add(a, c)) : Nat}
254	  %Equal.sym(Nat, Nat.add(a, b), Nat.add(b, a), add_comm(a, b)) :
255	    {Nat.add(_, c) == Nat.add(b, Nat.add(a, c)) : Nat}
256	  add_assoc(b, a, c)
257	
258	law add_swap:
259	  for +a: Nat
260	  for +b: Nat
261	  for +c: Nat
262	  for +d: Nat
263	  {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}
264	
265	def add_swap(a, b, c, d):
266	  %Equal.sym(Nat, Nat.add(Nat.add(a, b), Nat.add(c, d)), Nat.add(a, Nat.add(b, Nat.add(c, d))), add_assoc(a, b, Nat.add(c, d))) :
267	    {_ == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}
268	  %Equal.sym(Nat, Nat.add(Nat.add(a, c), Nat.add(b, d)), Nat.add(a, Nat.add(c, Nat.add(b, d))), add_assoc(a, c, Nat.add(b, d))) :
269	    {Nat.add(a, Nat.add(b, Nat.add(c, d))) == _ : Nat}
270	  %Equal.sym(Nat, Nat.add(b, Nat.add(c, d)), Nat.add(c, Nat.add(b, d)), add_left_comm(b, c, d)) :
271	    {Nat.add(a, _) == Nat.add(a, Nat.add(c, Nat.add(b, d))) : Nat}
272	  {==}
273	
274	# a + x = a + y gives x = y.
275	law add_cancel_l:
276	  for +a: Nat
277	  for +x: Nat
278	  for +y: Nat
279	  for e: {Nat.add(a, x) == Nat.add(a, y) : Nat}
280	  {x == y : Nat}
281	
282	def add_cancel_l(a, x, y, e):
283	  match a:
284	    case 0n:
285	      e
286	    case 1n+p:
287	      add_cancel_l(p, x, y, succ_inj(Nat.add(p, x), Nat.add(p, y), e))
288	
289	# x + a = y + a gives x = y.
290	law add_cancel_r:
291	  for +a: Nat
292	  for +x: Nat
293	  for +y: Nat
294	  for e: {Nat.add(x, a) == Nat.add(y, a) : Nat}
295	  {x == y : Nat}
296	
297	def add_cancel_r(a, x, y, e):
298	  add_cancel_l(a, x, y,
299	    %add_comm(x, a) : {_ == Nat.add(a, y) : Nat}
300	    %add_comm(y, a) : {Nat.add(x, a) == _ : Nat}
301	    e)
302	
303	# x + y = x gives y = 0.
304	law add_self_r:
305	  for +x: Nat
306	  for +y: Nat
307	  for e: {Nat.add(x, y) == x : Nat}
308	  {y == 0n : Nat}
309	
310	def add_self_r(x, y, e):
311	  add_cancel_l(x, y, 0n,
312	    %Equal.sym(Nat, Nat.add(x, 0n), x, add_zero(x)) : {Nat.add(x, y) == _ : Nat}
313	    e)
314	
315	# x + y = 0 gives x = 0 (and y = 0).
316	law add_eq_zero_l:
317	  for +x: Nat
318	  for +y: Nat
319	  for e: {Nat.add(x, y) == 0n : Nat}
320	  {x == 0n : Nat}
321	
322	def add_eq_zero_l(x, y, e):
323	  match x:
324	    case 0n:
325	      {==}
326	    case 1n+p:
327	      Empty.absurd({1n+p == 0n : Nat}, succ_ne_zero(Nat.add(p, y), e))
328	
329	law add_eq_zero_r:
330	  for +x: Nat
331	  for +y: Nat
332	  for e: {Nat.add(x, y) == 0n : Nat}
333	  {y == 0n : Nat}
334	
335	def add_eq_zero_r(x, y, e):
336	  match x:
337	    case 0n:
338	      e
339	    case 1n+p:
340	      Empty.absurd({y == 0n : Nat}, succ_ne_zero(Nat.add(p, y), e))
341	
342	# Nat: subtraction
343	# ================
344	
345	law sub_zero:
346	  for +i: Nat
347	  {Nat.sub(i, 0n) == i : Nat}
348	
349	def sub_zero(i):
350	  match i:
351	    case 0n:
352	      {==}
353	    case 1n+k:
354	      {==}
355	
356	# (x + y) - y = x.
357	law sub_add:
358	  for +x: Nat
359	  for +y: Nat
360	  {Nat.sub(Nat.add(x, y), y) == x : Nat}
361	
362	def sub_add(x, y):
363	  match y:
364	    case 0n:
365	      %Equal.sym(Nat, Nat.add(x, 0n), x, add_zero(x)) : {Nat.sub(_, 0n) == x : Nat}
366	      sub_zero(x)
367	    case 1n+q:
368	      %Equal.sym(Nat, Nat.add(x, 1n+q), 1n+Nat.add(x, q), add_succ(x, q)) :
369	        {Nat.sub(_, 1n+q) == x : Nat}
370	      sub_add(x, q)
371	
372	# (y + x) - y = x.
373	law sub_add_l:
374	  for +y: Nat
375	  for +x: Nat
376	  {Nat.sub(Nat.add(y, x), y) == x : Nat}
377	
378	def sub_add_l(y, x):
379	  %add_comm(x, y) : {Nat.sub(_, y) == x : Nat}
380	  sub_add(x, y)
381	
382	# Nat: multiplication
383	# ===================
384	
385	law mul_zero_r:
386	  for +a: Nat
387	  {Nat.mul(a, 0n) == 0n : Nat}
388	
389	def mul_zero_r(a):
390	  match a:
391	    case 0n:
392	      {==}
393	    case 1n+p:
394	      mul_zero_r(p)
395	
396	law mul_succ_r:
397	  for +a: Nat
398	  for +b: Nat
399	  {Nat.mul(a, 1n+b) == Nat.add(a, Nat.mul(a, b)) : Nat}
400	
401	def mul_succ_r(a, b):
402	  match a:
403	    case 0n:
404	      {==}
405	    case 1n+p:
406	      +x = Nat.mul(p, b)
407	      %Equal.sym(Nat, Nat.mul(p, 1n+b), Nat.add(p, x), mul_succ_r(p, b)) :
408	        {1n+Nat.add(b, _) == 1n+Nat.add(p, Nat.add(b, x)) : Nat}
409	      %Equal.sym(Nat, Nat.add(b, Nat.add(p, x)), Nat.add(p, Nat.add(b, x)), add_left_comm(b, p, x)) :
410	        {1n+_ == 1n+Nat.add(p, Nat.add(b, x)) : Nat}
411	      {==}
412	
413	law mul_comm:
414	  for +a: Nat
415	  for +b: Nat
416	  {Nat.mul(a, b) == Nat.mul(b, a) : Nat}
417	
418	def mul_comm(a, b):
419	  match a:
420	    case 0n:
421	      Equal.sym(Nat, Nat.mul(b, 0n), 0n, mul_zero_r(b))
422	    case 1n+p:
423	      %Equal.sym(Nat, Nat.mul(p, b), Nat.mul(b, p), mul_comm(p, b)) :
424	        {Nat.add(b, _) == Nat.mul(b, 1n+p) : Nat}
425	      Equal.sym(Nat, Nat.mul(b, 1n+p), Nat.add(b, Nat.mul(b, p)), mul_succ_r(b, p))
426	
427	law mul_one:
428	  for +a: Nat
429	  {Nat.mul(a, 1n) == a : Nat}
430	
431	def mul_one(a):
432	  match a:
433	    case 0n:
434	      {==}
435	    case 1n+p:
436	      %mul_one(p) : {1n+Nat.mul(p, 1n) == 1n+_ : Nat}
437	      {==}
438	
439	law mul_add:
440	  for +a: Nat
441	  for +b: Nat
442	  for +c: Nat
443	  {Nat.mul(a, Nat.add(b, c)) == Nat.add(Nat.mul(a, b), Nat.mul(a, c)) : Nat}
444	
445	def mul_add(a, b, c):
446	  match a:
447	    case 0n:
448	      {==}
449	    case 1n+p:
450	      %Equal.sym(Nat, Nat.mul(p, Nat.add(b, c)), Nat.add(Nat.mul(p, b), Nat.mul(p, c)), mul_add(p, b, c)) : {Nat.add(Nat.add(b, c), _) == Nat.add(Nat.add(b, Nat.mul(p, b)), Nat.add(c, Nat.mul(p, c))) : Nat}
451	      add_swap(b, c, Nat.mul(p, b), Nat.mul(p, c))
452	
453	law mul_add_r:
454	  for +a: Nat
455	  for +b: Nat
456	  for +c: Nat
457	  {Nat.mul(Nat.add(a, b), c) == Nat.add(Nat.mul(a, c), Nat.mul(b, c)) : Nat}
458	
459	def mul_add_r(a, b, c):
460	  match a:
461	    case 0n:
462	      {==}
463	    case 1n+p:
464	      %Equal.sym(Nat, Nat.mul(Nat.add(p, b), c), Nat.add(Nat.mul(p, c), Nat.mul(b, c)), mul_add_r(p, b, c)) :
465	        {Nat.add(c, _) == Nat.add(Nat.add(c, Nat.mul(p, c)), Nat.mul(b, c)) : Nat}
466	      Equal.sym(Nat, Nat.add(Nat.add(c, Nat.mul(p, c)), Nat.mul(b, c)), Nat.add(c, Nat.add(Nat.mul(p, c), Nat.mul(b, c))),
467	        add_assoc(c, Nat.mul(p, c), Nat.mul(b, c)))
468	
469	law mul_assoc:
470	  for +a: Nat
471	  for +b: Nat
472	  for +c: Nat
473	  {Nat.mul(Nat.mul(a, b), c) == Nat.mul(a, Nat.mul(b, c)) : Nat}
474	
475	def mul_assoc(a, b, c):
476	  match a:
477	    case 0n:
478	      {==}
479	    case 1n+p:
480	      %Equal.sym(Nat, Nat.mul(Nat.add(b, Nat.mul(p, b)), c), Nat.add(Nat.mul(b, c), Nat.mul(Nat.mul(p, b), c)), mul_add_r(b, Nat.mul(p, b), c)) :
481	        {_ == Nat.add(Nat.mul(b, c), Nat.mul(p, Nat.mul(b, c))) : Nat}
482	      %mul_assoc(p, b, c) : {Nat.add(Nat.mul(b, c), Nat.mul(Nat.mul(p, b), c)) == Nat.add(Nat.mul(b, c), _) : Nat}
483	      {==}
484	
485	# Doubling
486	# ========
487	
488	law dbl_add:
489	  for +x: Nat
490	  {Nat.double(x) == Nat.add(x, x) : Nat}
491	
492	def dbl_add(x):
493	  match x:
494	    case 0n:
495	      {==}
496	    case 1n+p:
497	      %Equal.sym(Nat, Nat.add(p, 1n+p), 1n+Nat.add(p, p), add_succ(p, p)) : {2n+Nat.double(p) == 1n+_ : Nat}
498	      %dbl_add(p) : {2n+Nat.double(p) == 2n+_ : Nat}
499	      {==}
500	
501	law dbl_dist:
502	  for +x: Nat
503	  for +y: Nat
504	  {Nat.double(Nat.add(x, y)) == Nat.add(Nat.double(x), Nat.double(y)) : Nat}
505	
506	def dbl_dist(x, y):
507	  match x:
508	    case 0n:
509	      {==}
510	    case 1n+p:
511	      %dbl_dist(p, y) : {2n+Nat.double(Nat.add(p, y)) == 2n+_ : Nat}
512	      {==}
513	
514	law mul2:
515	  for +x: Nat
516	  {Nat.mul(2n, x) == Nat.double(x) : Nat}
517	
518	def mul2(x):
519	  %Equal.sym(Nat, Nat.add(x, 0n), x, add_zero(x)) : {Nat.add(x, _) == Nat.double(x) : Nat}
520	  Equal.sym(Nat, Nat.double(x), Nat.add(x, x), dbl_add(x))
521	
522	law mul2_r:
523	  for +x: Nat
524	  {Nat.mul(x, 2n) == Nat.double(x) : Nat}
525	
526	def mul2_r(x):
527	  %mul_comm(2n, x) : {_ == Nat.double(x) : Nat}
528	  mul2(x)
529	
530	law mul_dbl_r:
531	  for +a: Nat
532	  for +x: Nat
533	  {Nat.mul(a, Nat.double(x)) == Nat.double(Nat.mul(a, x)) : Nat}
534	
535	def mul_dbl_r(a, x):
536	  match a:
537	    case 0n:
538	      {==}
539	    case 1n+p:
540	      %Equal.sym(Nat, Nat.mul(p, Nat.double(x)), Nat.double(Nat.mul(p, x)), mul_dbl_r(p, x)) : {Nat.add(Nat.double(x), _) == Nat.double(Nat.add(x, Nat.mul(p, x))) : Nat}
541	      Equal.sym(Nat, Nat.double(Nat.add(x, Nat.mul(p, x))), Nat.add(Nat.double(x), Nat.double(Nat.mul(p, x))), dbl_dist(x, Nat.mul(p, x)))
542	
543	law mul_dbl_l:
544	  for +a: Nat
545	  for +x: Nat
546	  {Nat.mul(Nat.double(a), x) == Nat.double(Nat.mul(a, x)) : Nat}
547	
548	def mul_dbl_l(a, x):
549	  %mul_comm(x, Nat.double(a)) : {_ == Nat.double(Nat.mul(a, x)) : Nat}
550	  %mul_comm(x, a) : {Nat.mul(x, Nat.double(a)) == Nat.double(_) : Nat}
551	  mul_dbl_r(x, a)
552	
553	law dbl_inj:
554	  for +x: Nat
555	  for +y: Nat
556	  for e: {Nat.double(x) == Nat.double(y) : Nat}
557	  {x == y : Nat}
558	
559	def dbl_inj(x, y, e):
560	  match x y:
561	    case 0n 0n:
562	      {==}
563	    case 0n 1n+q:
564	      Empty.absurd({0n == 1n+q : Nat}, zero_ne_succ(1n+Nat.double(q), e))
565	    case 1n+p 0n:
566	      Empty.absurd({1n+p == 0n : Nat}, succ_ne_zero(1n+Nat.double(p), e))
567	    case 1n+p 1n+q:
568	      %dbl_inj(p, q, succ_inj(Nat.double(p), Nat.double(q), succ_inj(1n+Nat.double(p), 1n+Nat.double(q), e))) : {1n+p == 1n+_ : Nat}
569	      {==}
570	
571	law dbl_ne_odd:
572	  for +x: Nat
573	  for +y: Nat
574	  for e: {Nat.double(x) == 1n+Nat.double(y) : Nat}
575	  Empty
576	
577	def dbl_ne_odd(x, y, e):
578	  match x y:
579	    case 0n _:
580	      zero_ne_succ(Nat.double(y), e)
581	    case 1n+p 0n:
582	      succ_ne_zero(Nat.double(p), succ_inj(1n+Nat.double(p), 0n, e))
583	    case 1n+p 1n+q:
584	      dbl_ne_odd(p, q, succ_inj(Nat.double(p), 1n+Nat.double(q), succ_inj(1n+Nat.double(p), 2n+Nat.double(q), e)))
585	
586	law dbl_zero:
587	  for +x: Nat
588	  for e: {Nat.double(x) == 0n : Nat}
589	  {x == 0n : Nat}
590	
591	def dbl_zero(x, e):
592	  match x:
593	    case 0n:
594	      {==}
595	    case 1n+p:
596	      Empty.absurd({1n+p == 0n : Nat}, succ_ne_zero(1n+Nat.double(p), e))
597	
598	# Order
599	# =====
600	
601	law lt_zero:
602	  for +i: Nat
603	  {Nat.is_lt(i, 0n) == False{} : Bool}
604	
605	def lt_zero(i):
606	  match i:
607	    case 0n:
608	      {==}
609	    case 1n+k:
610	      {==}
611	
612	law lt_irrefl:
613	  for +n: Nat
614	  {Nat.is_lt(n, n) == False{} : Bool}
615	
616	def lt_irrefl(n):
617	  match n:
618	    case 0n:
619	      {==}
620	    case 1n+p:
621	      lt_irrefl(p)
622	
623	law le_zero_l:
624	  for +n: Nat
625	  {Nat.is_le(0n, n) == True{} : Bool}
626	
627	def le_zero_l(n):
628	  match n:
629	    case 0n:
630	      {==}
631	    case 1n+p:
632	      {==}
633	
634	law le_refl:
635	  for +a: Nat
636	  {Nat.is_le(a, a) == True{} : Bool}
637	
638	def le_refl(a):
639	  match a:
640	    case 0n:
641	      {==}
642	    case 1n+p:
643	      le_refl(p)
644	
645	# a < 1 + b is a <= b.
646	law lt_succ_iff:
647	  for +a: Nat
648	  for +b: Nat
649	  {Nat.is_lt(a, 1n+b) == Nat.is_le(a, b) : Bool}
650	
651	def lt_succ_iff(a, b):
652	  match a b:
653	    case 0n 0n:
654	      {==}
655	    case 0n 1n+q:
656	      {==}
657	    case 1n+p 0n:
658	      lt_zero(p)
659	    case 1n+p 1n+q:
660	      lt_succ_iff(p, q)
661	
662	# 1 + a <= b is a < b.
663	law le_succ_lt:
664	  for +a: Nat
665	  for +b: Nat
666	  {Nat.is_le(1n+a, b) == Nat.is_lt(a, b) : Bool}
667	
668	def le_succ_lt(a, b):
669	  match b:
670	    case 0n:
671	      Equal.sym(Bool, Nat.is_lt(a, 0n), False{}, lt_zero(a))
672	    case 1n+q:
673	      Equal.sym(Bool, Nat.is_lt(a, 1n+q), Nat.is_le(a, q), lt_succ_iff(a, q))
674	
675	# not (a < b) is b <= a.
676	law not_lt_le:
677	  for +a: Nat
678	  for +b: Nat
679	  for e: {Nat.is_lt(a, b) == False{} : Bool}
680	  {Nat.is_le(b, a) == True{} : Bool}
681	
682	def not_lt_le(a, b, e):
683	  match a b:
684	    case 0n 0n:
685	      {==}
686	    case 0n 1n+q:
687	      Empty.absurd({Nat.is_le(1n+q, 0n) == True{} : Bool}, true_ne_false(e))
688	    case 1n+p 0n:
689	      {==}
690	    case 1n+p 1n+q:
691	      not_lt_le(p, q, e)
692	
693	# not (a <= b) is b < a.
694	law not_le_lt:
695	  for +a: Nat
696	  for +b: Nat
697	  for e: {Nat.is_le(a, b) == False{} : Bool}
698	  {Nat.is_lt(b, a) == True{} : Bool}
699	
700	def not_le_lt(a, b, e):
701	  match a b:
702	    case 0n _:
703	      Empty.absurd({Nat.is_lt(b, 0n) == True{} : Bool}, true_ne_false(
704	        Equal.trans(Bool, True{}, Nat.is_le(0n, b), False{}, Equal.sym(Bool, Nat.is_le(0n, b), True{}, le_zero_l(b)), e)))
705	    case 1n+p 0n:
706	      {==}
707	    case 1n+p 1n+q:
708	      not_le_lt(p, q, e)
709	
710	law lt_to_le:
711	  for +a: Nat
712	  for +b: Nat
713	  for e: {Nat.is_lt(a, b) == True{} : Bool}
714	  {Nat.is_le(a, b) == True{} : Bool}
715	
716	def lt_to_le(a, b, e):
717	  match a b:
718	    case 0n _:
719	      le_zero_l(b)
720	    case 1n+p 0n:
721	      Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, false_ne_true(e))
722	    case 1n+p 1n+q:
723	      lt_to_le(p, q, e)
724	
725	law le_trans:
726	  for +a: Nat
727	  for +b: Nat
728	  for +c: Nat
729	  for ab: {Nat.is_le(a, b) == True{} : Bool}
730	  for bc: {Nat.is_le(b, c) == True{} : Bool}
731	  {Nat.is_le(a, c) == True{} : Bool}
732	
733	def le_trans(a, b, c, ab, bc):
734	  match a b c:
735	    case 0n _ _:
736	      le_zero_l(c)
737	    case 1n+p 0n _:
738	      Empty.absurd({Nat.is_le(1n+p, c) == True{} : Bool}, false_ne_true(ab))
739	    case 1n+p 1n+q 0n:
740	      Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, false_ne_true(bc))
741	    case 1n+p 1n+q 1n+r:
742	      le_trans(p, q, r, ab, bc)
743	
744	law lt_le_trans:
745	  for +a: Nat
746	  for +b: Nat
747	  for +c: Nat
748	  for ab: {Nat.is_lt(a, b) == True{} : Bool}
749	  for bc: {Nat.is_le(b, c) == True{} : Bool}
750	  {Nat.is_lt(a, c) == True{} : Bool}
751	
752	def lt_le_trans(a, b, c, ab, bc):
753	  %le_succ_lt(a, c) : {_ == True{} : Bool}
754	  le_trans(1n+a, b, c, %Equal.sym(Bool, Nat.is_le(1n+a, b), Nat.is_lt(a, b), le_succ_lt(a, b)) : {_ == True{} : Bool}; ab, bc)
755	
756	law le_lt_trans:
757	  for +a: Nat
758	  for +b: Nat
759	  for +c: Nat
760	  for ab: {Nat.is_le(a, b) == True{} : Bool}
761	  for bc: {Nat.is_lt(b, c) == True{} : Bool}
762	  {Nat.is_lt(a, c) == True{} : Bool}
763	
764	def le_lt_trans(a, b, c, ab, bc):
765	  %le_succ_lt(a, c) : {_ == True{} : Bool}
766	  le_trans(1n+a, 1n+b, c, ab, %Equal.sym(Bool, Nat.is_le(1n+b, c), Nat.is_lt(b, c), le_succ_lt(b, c)) : {_ == True{} : Bool}; bc)
767	
768	law lt_trans:
769	  for +a: Nat
770	  for +b: Nat
771	  for +c: Nat
772	  for ab: {Nat.is_lt(a, b) == True{} : Bool}
773	  for bc: {Nat.is_lt(b, c) == True{} : Bool}
774	  {Nat.is_lt(a, c) == True{} : Bool}
775	
776	def lt_trans(a, b, c, ab, bc):
777	  lt_le_trans(a, b, c, ab, lt_to_le(b, c, bc))
778	
779	# a <= a + k and a <= k + a.
780	law le_add_r:
781	  for +a: Nat
782	  for +k: Nat
783	  {Nat.is_le(a, Nat.add(a, k)) == True{} : Bool}
784	
785	def le_add_r(a, k):
786	  match a:
787	    case 0n:
788	      le_zero_l(k)
789	    case 1n+p:
790	      le_add_r(p, k)
791	
792	law le_add_l:
793	  for +a: Nat
794	  for +k: Nat
795	  {Nat.is_le(a, Nat.add(k, a)) == True{} : Bool}
796	
797	def le_add_l(a, k):
798	  %add_comm(a, k) : {Nat.is_le(a, _) == True{} : Bool}
799	  le_add_r(a, k)
800	
801	# b + x is never below b.
802	law lt_add_self:
803	  for +b: Nat
804	  for +x: Nat
805	  {Nat.is_lt(Nat.add(b, x), b) == False{} : Bool}
806	
807	def lt_add_self(b, x):
808	  match b:
809	    case 0n:
810	      lt_zero(x)
811	    case 1n+p:
812	      lt_add_self(p, x)
813	
814	law lt_pos:
815	  for +r: Nat
816	  for +b: Nat
817	  for h: {Nat.is_lt(r, b) == True{} : Bool}
818	  {Nat.is_lt(0n, b) == True{} : Bool}
819	
820	def lt_pos(r, b, h):
821	  match b:
822	    case 0n:
823	      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, false_ne_true(
824	        Equal.trans(Bool, False{}, Nat.is_lt(r, 0n), True{}, Equal.sym(Bool, Nat.is_lt(r, 0n), False{}, lt_zero(r)), h)))
825	    case 1n+q:
826	      {==}
827	
828	law pos_add_l:
829	  for +x: Nat
830	  for +y: Nat
831	  for h: {Nat.is_lt(0n, x) == True{} : Bool}
832	  {Nat.is_lt(0n, Nat.add(x, y)) == True{} : Bool}
833	
834	def pos_add_l(x, y, h):
835	  match x:
836	    case 0n:
837	      Empty.absurd({Nat.is_lt(0n, y) == True{} : Bool}, false_ne_true(h))
838	    case 1n+p:
839	      {==}
840	
841	# c + a < c + b from a < b (and the same for <=).
842	law lt_add_l:
843	  for +c: Nat
844	  for +a: Nat
845	  for +b: Nat
846	  for h: {Nat.is_lt(a, b) == True{} : Bool}
847	  {Nat.is_lt(Nat.add(c, a), Nat.add(c, b)) == True{} : Bool}
848	
849	def lt_add_l(c, a, b, h):
850	  match c:
851	    case 0n:
852	      h
853	    case 1n+p:
854	      lt_add_l(p, a, b, h)
855	
856	law le_add_mono_l:
857	  for +c: Nat
858	  for +a: Nat
859	  for +b: Nat
860	  for h: {Nat.is_le(a, b) == True{} : Bool}
861	  {Nat.is_le(Nat.add(c, a), Nat.add(c, b)) == True{} : Bool}
862	
863	def le_add_mono_l(c, a, b, h):
864	  match c:
865	    case 0n:
866	      h
867	    case 1n+p:
868	      le_add_mono_l(p, a, b, h)
869	
870	law le_add_mono_r:
871	  for +c: Nat
872	  for +a: Nat
873	  for +b: Nat
874	  for h: {Nat.is_le(a, b) == True{} : Bool}
875	  {Nat.is_le(Nat.add(a, c), Nat.add(b, c)) == True{} : Bool}
876	
877	def le_add_mono_r(c, a, b, h):
878	  %add_comm(c, a) : {Nat.is_le(_, Nat.add(b, c)) == True{} : Bool}
879	  %add_comm(c, b) : {Nat.is_le(Nat.add(c, a), _) == True{} : Bool}
880	  le_add_mono_l(c, a, b, h)
881	
882	law lt_add_mono_r:
883	  for +c: Nat
884	  for +a: Nat
885	  for +b: Nat
886	  for h: {Nat.is_lt(a, b) == True{} : Bool}
887	  {Nat.is_lt(Nat.add(a, c), Nat.add(b, c)) == True{} : Bool}
888	
889	def lt_add_mono_r(c, a, b, h):
890	  %add_comm(c, a) : {Nat.is_lt(_, Nat.add(b, c)) == True{} : Bool}
891	  %add_comm(c, b) : {Nat.is_lt(Nat.add(c, a), _) == True{} : Bool}
892	  lt_add_l(c, a, b, h)
893	
894	# a <= b gives a * c <= b * c.
895	law le_mul_r:
896	  for +a: Nat
897	  for +b: Nat
898	  for +c: Nat
899	  for e: {Nat.is_le(a, b) == True{} : Bool}
900	  {Nat.is_le(Nat.mul(a, c), Nat.mul(b, c)) == True{} : Bool}
901	
902	def le_mul_r(a, b, c, e):
903	  match a b:
904	    case 0n _:
905	      le_zero_l(Nat.mul(b, c))
906	    case 1n+p 0n:
907	      Empty.absurd({Nat.is_le(Nat.mul(1n+p, c), 0n) == True{} : Bool}, false_ne_true(e))
908	    case 1n+p 1n+q:
909	      le_add_mono_l(c, Nat.mul(p, c), Nat.mul(q, c), le_mul_r(p, q, c, e))
910	
911	law le_mul_l:
912	  for +c: Nat
913	  for +a: Nat
914	  for +b: Nat
915	  for e: {Nat.is_le(a, b) == True{} : Bool}
916	  {Nat.is_le(Nat.mul(c, a), Nat.mul(c, b)) == True{} : Bool}
917	
918	def le_mul_l(c, a, b, e):
919	  %mul_comm(a, c) : {Nat.is_le(_, Nat.mul(c, b)) == True{} : Bool}
920	  %mul_comm(b, c) : {Nat.is_le(Nat.mul(a, c), _) == True{} : Bool}
921	  le_mul_r(a, b, c, e)
922	
923	# k <= m gives k + (m - k) = m.
924	law le_sub_add:
925	  for +k: Nat
926	  for +m: Nat
927	  for h: {Nat.is_le(k, m) == True{} : Bool}
928	  {Nat.add(k, Nat.sub(m, k)) == m : Nat}
929	
930	def le_sub_add(k, m, h):
931	  match k m:
932	    case 0n _:
933	      sub_zero(m)
934	    case 1n+p 0n:
935	      Empty.absurd({Nat.add(1n+p, Nat.sub(0n, 1n+p)) == 0n : Nat}, false_ne_true(h))
936	    case 1n+p 1n+q:
937	      %le_sub_add(p, q, h) : {1n+Nat.add(p, Nat.sub(q, p)) == 1n+_ : Nat}
938	      {==}
939	
940	# Division and remainder
941	# ======================
942	
943	# The loop of Nat.divmod keeps d * b + r + n, with b = 1 + bp and m + r = bp.
944	law go_eq:
945	  for +n: Nat
946	  for +m: Nat
947	  for +d: Nat
948	  for +r: Nat
949	  for +bp: Nat
950	  for +h: {Nat.add(m, r) == bp : Nat}
951	  {Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(n, m, d, r)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d, r)))
952	    == Nat.add(Nat.mul(d, 1n+bp), Nat.add(r, n)) : Nat}
953	
954	def go_eq(n, m, d, r, bp, h):
955	  match n:
956	    case 0n:
957	      %Equal.sym(Nat, Nat.add(r, 0n), r, add_zero(r)) : {Nat.add(Nat.mul(d, 1n+bp), r) == Nat.add(Nat.mul(d, 1n+bp), _) : Nat}
958	      {==}
959	    case 1n+np:
960	      match m:
961	        case 0n:
962	          -g = Nat.divmod.go(np, r, 1n+d, 0n)
963	          +db = Nat.mul(d, 1n+bp)
964	          Equal.trans(Nat, Nat.add(Nat.mul(Pair.fst(Nat, Nat, g), 1n+bp), Pair.snd(Nat, Nat, g)),
965	            Nat.add(Nat.mul(1n+d, 1n+bp), Nat.add(0n, np)), Nat.add(db, Nat.add(r, 1n+np)),
966	            go_eq(np, r, 1n+d, 0n, bp, %Equal.sym(Nat, Nat.add(r, 0n), r, add_zero(r)) : {_ == bp : Nat}; h),
967	            %Equal.sym(Nat, r, bp, h) : {Nat.add(Nat.add(1n+bp, db), np) == Nat.add(db, Nat.add(_, 1n+np)) : Nat}
968	            %Equal.sym(Nat, Nat.add(bp, 1n+np), 1n+Nat.add(bp, np), add_succ(bp, np)) :
969	              {Nat.add(Nat.add(1n+bp, db), np) == Nat.add(db, _) : Nat}
970	            %Equal.sym(Nat, Nat.add(db, 1n+Nat.add(bp, np)), 1n+Nat.add(db, Nat.add(bp, np)), add_succ(db, Nat.add(bp, np))) :
971	              {Nat.add(Nat.add(1n+bp, db), np) == _ : Nat}
972	            %Equal.sym(Nat, Nat.add(Nat.add(bp, db), np), Nat.add(bp, Nat.add(db, np)), add_assoc(bp, db, np)) :
973	              {1n+_ == 1n+Nat.add(db, Nat.add(bp, np)) : Nat}
974	            %add_left_comm(bp, db, np) : {1n+Nat.add(bp, Nat.add(db, np)) == 1n+_ : Nat}
975	            {==})
976	        case 1n+mp:
977	          -g = Nat.divmod.go(np, mp, d, 1n+r)
978	          +db = Nat.mul(d, 1n+bp)
979	          Equal.trans(Nat, Nat.add(Nat.mul(Pair.fst(Nat, Nat, g), 1n+bp), Pair.snd(Nat, Nat, g)),
980	            Nat.add(db, Nat.add(1n+r, np)), Nat.add(db, Nat.add(r, 1n+np)),
981	            go_eq(np, mp, d, 1n+r, bp, %Equal.sym(Nat, Nat.add(mp, 1n+r), 1n+Nat.add(mp, r), add_succ(mp, r)) : {_ == bp : Nat}; h),
982	            %Equal.sym(Nat, Nat.add(r, 1n+np), 1n+Nat.add(r, np), add_succ(r, np)) : {Nat.add(db, 1n+Nat.add(r, np)) == Nat.add(db, _) : Nat}
983	            {==})
984	
985	law go_lt:
986	  for +n: Nat
987	  for +m: Nat
988	  for +d: Nat
989	  for +r: Nat
990	  for +bp: Nat
991	  for +h: {Nat.add(m, r) == bp : Nat}
992	  {Nat.is_lt(Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d, r)), 1n+bp) == True{} : Bool}
993	
994	def go_lt(n, m, d, r, bp, h):
995	  match n:
996	    case 0n:
997	      %h : {Nat.is_lt(r, 1n+_) == True{} : Bool}
998	      %Equal.sym(Bool, Nat.is_lt(r, 1n+Nat.add(m, r)), Nat.is_le(r, Nat.add(m, r)), lt_succ_iff(r, Nat.add(m, r))) : {_ == True{} : Bool}
999	      le_add_l(r, m)
1000	    case 1n+np:
1001	      match m:
1002	        case 0n:
1003	          go_lt(np, r, 1n+d, 0n, bp, %Equal.sym(Nat, Nat.add(r, 0n), r, add_zero(r)) : {_ == bp : Nat}; h)
1004	        case 1n+mp:
1005	          go_lt(np, mp, d, 1n+r, bp, %Equal.sym(Nat, Nat.add(mp, 1n+r), 1n+Nat.add(mp, r), add_succ(mp, r)) : {_ == bp : Nat}; h)
1006	
1007	# a = (a / b) * b + a % b.
1008	law div_mod:
1009	  for +a: Nat
1010	  for +b: Nat
1011	  {Nat.add(Nat.mul(Nat.div(a, b), b), Nat.mod(a, b)) == a : Nat}
1012	
1013	def div_mod(a, b):
1014	  match b:
1015	    case 0n:
1016	      {==}
1017	    case 1n+bp:
1018	      go_eq(a, bp, 0n, 0n, bp, add_zero(bp))
1019	
1020	law mod_lt:
1021	  for +a: Nat
1022	  for +b: Nat
1023	  for h: {Nat.is_lt(0n, b) == True{} : Bool}
1024	  {Nat.is_lt(Nat.mod(a, b), b) == True{} : Bool}
1025	
1026	def mod_lt(a, b, h):
1027	  match b:
1028	    case 0n:
1029	      Empty.absurd({Nat.is_lt(Nat.mod(a, 0n), 0n) == True{} : Bool}, false_ne_true(h))
1030	    case 1n+bp:
1031	      go_lt(a, bp, 0n, 0n, bp, add_zero(bp))
1032	
1033	# q1 * b + r1 = q2 * b + r2 with r1, r2 < b gives q1 = q2.
1034	law div_uniq:
1035	  for +q1: Nat
1036	  for +q2: Nat
1037	  for +b: Nat
1038	  for +r1: Nat
1039	  for +r2: Nat
1040	  for h1: {Nat.is_lt(r1, b) == True{} : Bool}
1041	  for h2: {Nat.is_lt(r2, b) == True{} : Bool}
1042	  for e: {Nat.add(Nat.mul(q1, b), r1) == Nat.add(Nat.mul(q2, b), r2) : Nat}
1043	  {q1 == q2 : Nat}
1044	
1045	def div_uniq(q1, q2, b, r1, r2, h1, h2, e):
1046	  match q1 q2:
1047	    case 0n 0n:
1048	      {==}
1049	    case 0n 1n+q:
1050	      +x = Nat.mul(q, b)
1051	      Empty.absurd({0n == 1n+q : Nat}, false_ne_true(Equal.trans(Bool, False{}, Nat.is_lt(Nat.add(b, Nat.add(x, r2)), b), True{},
1052	        Equal.sym(Bool, Nat.is_lt(Nat.add(b, Nat.add(x, r2)), b), False{}, lt_add_self(b, Nat.add(x, r2))),
1053	        %add_assoc(b, x, r2) : {Nat.is_lt(_, b) == True{} : Bool}
1054	        %e : {Nat.is_lt(_, b) == True{} : Bool}
1055	        h1)))
1056	    case 1n+p 0n:
1057	      +x = Nat.mul(p, b)
1058	      Empty.absurd({1n+p == 0n : Nat}, false_ne_true(Equal.trans(Bool, False{}, Nat.is_lt(Nat.add(b, Nat.add(x, r1)), b), True{},
1059	        Equal.sym(Bool, Nat.is_lt(Nat.add(b, Nat.add(x, r1)), b), False{}, lt_add_self(b, Nat.add(x, r1))),
1060	        %add_assoc(b, x, r1) : {Nat.is_lt(_, b) == True{} : Bool}
1061	        %Equal.sym(Nat, Nat.add(Nat.add(b, x), r1), r2, e) : {Nat.is_lt(_, b) == True{} : Bool}
1062	        h2)))
1063	    case 1n+p 1n+q:
1064	      +x = Nat.mul(p, b)
1065	      +y = Nat.mul(q, b)
1066	      %div_uniq(p, q, b, r1, r2, h1, h2, add_cancel_l(b, Nat.add(x, r1), Nat.add(y, r2),
1067	        %add_assoc(b, x, r1) : {_ == Nat.add(b, Nat.add(y, r2)) : Nat}
1068	        %add_assoc(b, y, r2) : {Nat.add(Nat.add(b, x), r1) == _ : Nat}
1069	        e)) : {1n+p == 1n+_ : Nat}
1070	      {==}
1071	
1072	law div_mul_add:
1073	  for +q: Nat
1074	  for +b: Nat
1075	  for +r: Nat
1076	  for +h: {Nat.is_lt(r, b) == True{} : Bool}
1077	  {Nat.div(Nat.add(Nat.mul(q, b), r), b) == q : Nat}
1078	
1079	def div_mul_add(q, b, r, h):
1080	  +n = Nat.add(Nat.mul(q, b), r)
1081	  div_uniq(Nat.div(n, b), q, b, Nat.mod(n, b), r, mod_lt(n, b, lt_pos(r, b, h)), h, div_mod(n, b))
1082	
1083	law mod_mul_add:
1084	  for +q: Nat
1085	  for +b: Nat
1086	  for +r: Nat
1087	  for +h: {Nat.is_lt(r, b) == True{} : Bool}
1088	  {Nat.mod(Nat.add(Nat.mul(q, b), r), b) == r : Nat}
1089	
1090	def mod_mul_add(q, b, r, h):
1091	  +n = Nat.add(Nat.mul(q, b), r)
1092	  add_cancel_l(Nat.mul(q, b), Nat.mod(n, b), r,
1093	    %div_mul_add(q, b, r, h) : {Nat.add(Nat.mul(_, b), Nat.mod(n, b)) == n : Nat}
1094	    div_mod(n, b))
1095	
1096	law mod_small:
1097	  for +a: Nat
1098	  for +b: Nat
1099	  for +h: {Nat.is_lt(a, b) == True{} : Bool}
1100	  {Nat.mod(a, b) == a : Nat}
1101	
1102	def mod_small(a, b, h):
1103	  mod_mul_add(0n, b, a, h)
1104	
1105	law div_small:
1106	  for +a: Nat
1107	  for +b: Nat
1108	  for +h: {Nat.is_lt(a, b) == True{} : Bool}
1109	  {Nat.div(a, b) == 0n : Nat}
1110	
1111	def div_small(a, b, h):
1112	  div_mul_add(0n, b, a, h)
1113	
1114	law mul_mod:
1115	  for +a: Nat
1116	  for +b: Nat
1117	  {Nat.mod(Nat.mul(a, b), b) == 0n : Nat}
1118	
1119	def mul_mod(a, b):
1120	  match b:
1121	    case 0n:
1122	      mul_zero_r(a)
1123	    case 1n+bp:
1124	      %add_zero(Nat.mul(a, 1n+bp)) : {Nat.mod(_, 1n+bp) == 0n : Nat}
1125	      mod_mul_add(a, 1n+bp, 0n, {==})
1126	
1127	law div_mul:
1128	  for +a: Nat
1129	  for +b: Nat
1130	  for +h: {Nat.is_lt(0n, b) == True{} : Bool}
1131	  {Nat.div(Nat.mul(a, b), b) == a : Nat}
1132	
1133	def div_mul(a, b, h):
1134	  %add_zero(Nat.mul(a, b)) : {Nat.div(_, b) == a : Nat}
1135	  div_mul_add(a, b, 0n, h)
1136	
1137	law mod_one:
1138	  for +a: Nat
1139	  {Nat.mod(a, 1n) == 0n : Nat}
1140	
1141	def mod_one(a):
1142	  %mul_one(a) : {Nat.mod(_, 1n) == 0n : Nat}
1143	  mul_mod(a, 1n)
1144	
1145	law div_one:
1146	  for +a: Nat
1147	  {Nat.div(a, 1n) == a : Nat}
1148	
1149	def div_one(a):
1150	  %mul_one(a) : {Nat.div(_, 1n) == a : Nat}
1151	  div_mul(a, 1n, {==})
1152	
1153	law mod_zero_l:
1154	  for +b: Nat
1155	  {Nat.mod(0n, b) == 0n : Nat}
1156	
1157	def mod_zero_l(b):
1158	  match b:
1159	    case 0n:
1160	      {==}
1161	    case 1n+bp:
1162	      {==}
1163	
1164	law div_zero_l:
1165	  for +b: Nat
1166	  {Nat.div(0n, b) == 0n : Nat}
1167	
1168	def div_zero_l(b):
1169	  match b:
1170	    case 0n:
1171	      {==}
1172	    case 1n+bp:
1173	      {==}
1174	
1175	# Adding a multiple of x does not change the remainder by x.
1176	law mod_add_mul:
1177	  for +j: Nat
1178	  for +x: Nat
1179	  for +z: Nat
1180	  {Nat.mod(Nat.add(Nat.mul(j, x), z), x) == Nat.mod(z, x) : Nat}
1181	
1182	def mod_add_mul(j, x, z):
1183	  match x:
1184	    case 0n:
1185	      %Equal.sym(Nat, Nat.mul(j, 0n), 0n, mul_zero_r(j)) : {Nat.add(_, z) == z : Nat}
1186	      {==}
1187	    case 1n+xp:
1188	      +q = Nat.div(z, 1n+xp)
1189	      +r = Nat.mod(z, 1n+xp)
1190	      %div_mod(z, 1n+xp) : {Nat.mod(Nat.add(Nat.mul(j, 1n+xp), _), 1n+xp) == r : Nat}
1191	      %Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(j, q), 1n+xp), r), Nat.add(Nat.add(Nat.mul(j, 1n+xp), Nat.mul(q, 1n+xp)), r),
1192	          Nat.add(Nat.mul(j, 1n+xp), Nat.add(Nat.mul(q, 1n+xp), r)),
1193	          Equal.cong(Nat, Nat, t => Nat.add(t, r), Nat.mul(Nat.add(j, q), 1n+xp), Nat.add(Nat.mul(j, 1n+xp), Nat.mul(q, 1n+xp)), mul_add_r(j, q, 1n+xp)),
1194	          add_assoc(Nat.mul(j, 1n+xp), Nat.mul(q, 1n+xp), r)) :
1195	        {Nat.mod(_, 1n+xp) == r : Nat}
1196	      mod_mul_add(Nat.add(j, q), 1n+xp, r, mod_lt(z, 1n+xp, {==}))
1197	
1198	law div_add_mul:
1199	  for +j: Nat
1200	  for +x: Nat
1201	  for +z: Nat
1202	  for +h: {Nat.is_lt(0n, x) == True{} : Bool}
1203	  {Nat.div(Nat.add(Nat.mul(j, x), z), x) == Nat.add(j, Nat.div(z, x)) : Nat}
1204	
1205	def div_add_mul(j, x, z, h):
1206	  +q = Nat.div(z, x)
1207	  +r = Nat.mod(z, x)
1208	  %div_mod(z, x) : {Nat.div(Nat.add(Nat.mul(j, x), _), x) == Nat.add(j, q) : Nat}
1209	  %Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(j, q), x), r), Nat.add(Nat.add(Nat.mul(j, x), Nat.mul(q, x)), r),
1210	      Nat.add(Nat.mul(j, x), Nat.add(Nat.mul(q, x), r)),
1211	      Equal.cong(Nat, Nat, t => Nat.add(t, r), Nat.mul(Nat.add(j, q), x), Nat.add(Nat.mul(j, x), Nat.mul(q, x)), mul_add_r(j, q, x)),
1212	      add_assoc(Nat.mul(j, x), Nat.mul(q, x), r)) :
1213	    {Nat.div(_, x) == Nat.add(j, q) : Nat}
1214	  div_mul_add(Nat.add(j, q), x, r, mod_lt(z, x, h))
1215	
1216	# Remainders inside sums and products.
1217	law mod_add_mod_l:
1218	  for +u: Nat
1219	  for +v: Nat
1220	  for +m: Nat
1221	  {Nat.mod(Nat.add(Nat.mod(u, m), v), m) == Nat.mod(Nat.add(u, v), m) : Nat}
1222	
1223	def mod_add_mod_l(u, v, m):
1224	  +q = Nat.div(u, m)
1225	  +r = Nat.mod(u, m)
1226	  %div_mod(u, m) : {Nat.mod(Nat.add(r, v), m) == Nat.mod(Nat.add(_, v), m) : Nat}
1227	  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(q, m), r), v), Nat.add(Nat.mul(q, m), Nat.add(r, v)), add_assoc(Nat.mul(q, m), r, v)) :
1228	    {Nat.mod(Nat.add(r, v), m) == Nat.mod(_, m) : Nat}
1229	  Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(q, m), Nat.add(r, v)), m), Nat.mod(Nat.add(r, v), m), mod_add_mul(q, m, Nat.add(r, v)))
1230	
1231	law mod_add_mod_r:
1232	  for +v: Nat
1233	  for +u: Nat
1234	  for +m: Nat
1235	  {Nat.mod(Nat.add(v, Nat.mod(u, m)), m) == Nat.mod(Nat.add(v, u), m) : Nat}
1236	
1237	def mod_add_mod_r(v, u, m):
1238	  %add_comm(Nat.mod(u, m), v) : {Nat.mod(_, m) == Nat.mod(Nat.add(v, u), m) : Nat}
1239	  %add_comm(u, v) : {Nat.mod(Nat.add(Nat.mod(u, m), v), m) == Nat.mod(_, m) : Nat}
1240	  mod_add_mod_l(u, v, m)
1241	
1242	law mod_mul_mod_l:
1243	  for +u: Nat
1244	  for +y: Nat
1245	  for +m: Nat
1246	  {Nat.mod(Nat.mul(Nat.mod(u, m), y), m) == Nat.mod(Nat.mul(u, y), m) : Nat}
1247	
1248	def mod_mul_mod_l(u, y, m):
1249	  +q = Nat.div(u, m)
1250	  +r = Nat.mod(u, m)
1251	  %div_mod(u, m) : {Nat.mod(Nat.mul(r, y), m) == Nat.mod(Nat.mul(_, y), m) : Nat}
1252	  %Equal.sym(Nat, Nat.mul(Nat.add(Nat.mul(q, m), r), y), Nat.add(Nat.mul(Nat.mul(q, m), y), Nat.mul(r, y)), mul_add_r(Nat.mul(q, m), r, y)) :
1253	    {Nat.mod(Nat.mul(r, y), m) == Nat.mod(_, m) : Nat}
1254	  %Equal.trans(Nat, Nat.mul(Nat.mul(q, y), m), Nat.mul(q, Nat.mul(y, m)), Nat.mul(Nat.mul(q, m), y),
1255	      mul_assoc(q, y, m),
1256	      %mul_comm(m, y) : {Nat.mul(q, _) == Nat.mul(Nat.mul(q, m), y) : Nat}
1257	      Equal.sym(Nat, Nat.mul(Nat.mul(q, m), y), Nat.mul(q, Nat.mul(m, y)), mul_assoc(q, m, y))) :
1258	    {Nat.mod(Nat.mul(r, y), m) == Nat.mod(Nat.add(_, Nat.mul(r, y)), m) : Nat}
1259	  Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(Nat.mul(q, y), m), Nat.mul(r, y)), m), Nat.mod(Nat.mul(r, y), m), mod_add_mul(Nat.mul(q, y), m, Nat.mul(r, y)))
1260	
1261	law mod_mul_mod_r:
1262	  for +y: Nat
1263	  for +u: Nat
1264	  for +m: Nat
1265	  {Nat.mod(Nat.mul(y, Nat.mod(u, m)), m) == Nat.mod(Nat.mul(y, u), m) : Nat}
1266	
1267	def mod_mul_mod_r(y, u, m):
1268	  %mul_comm(Nat.mod(u, m), y) : {Nat.mod(_, m) == Nat.mod(Nat.mul(y, u), m) : Nat}
1269	  %mul_comm(u, y) : {Nat.mod(Nat.mul(Nat.mod(u, m), y), m) == Nat.mod(_, m) : Nat}
1270	  mod_mul_mod_l(u, y, m)
1271	
1272	law mod_mod:
1273	  for +u: Nat
1274	  for +m: Nat
1275	  {Nat.mod(Nat.mod(u, m), m) == Nat.mod(u, m) : Nat}
1276	
1277	def mod_mod(u, m):
1278	  %add_zero(Nat.mod(u, m)) : {Nat.mod(_, m) == Nat.mod(u, m) : Nat}
1279	  %add_zero(u) : {Nat.mod(Nat.add(Nat.mod(u, m), 0n), m) == Nat.mod(_, m) : Nat}
1280	  mod_add_mod_l(u, 0n, m)
1281	
1282	# (a % (x * y)) % x = a % x.
1283	law mod_mod_mul:
1284	  for +a: Nat
1285	  for +x: Nat
1286	  for +y: Nat
1287	  {Nat.mod(Nat.mod(a, Nat.mul(x, y)), x) == Nat.mod(a, x) : Nat}
1288	
1289	def mod_mod_mul(a, x, y):
1290	  +q = Nat.div(a, Nat.mul(x, y))
1291	  +r = Nat.mod(a, Nat.mul(x, y))
1292	  %div_mod(a, Nat.mul(x, y)) : {Nat.mod(r, x) == Nat.mod(_, x) : Nat}
1293	  %Equal.trans(Nat, Nat.mul(Nat.mul(q, y), x), Nat.mul(q, Nat.mul(y, x)), Nat.mul(q, Nat.mul(x, y)),
1294	      mul_assoc(q, y, x), %mul_comm(x, y) : {Nat.mul(q, _) == Nat.mul(q, Nat.mul(x, y)) : Nat}; {==}) :
1295	    {Nat.mod(r, x) == Nat.mod(Nat.add(_, r), x) : Nat}
1296	  Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(Nat.mul(q, y), x), r), x), Nat.mod(r, x), mod_add_mul(Nat.mul(q, y), x, r))
1297	
1298	# (a / x) / y = a / (x * y).
1299	law div_div:
1300	  for +a: Nat
1301	  for +x: Nat
1302	  for +y: Nat
1303	  {Nat.div(Nat.div(a, x), y) == Nat.div(a, Nat.mul(x, y)) : Nat}
1304	
1305	def div_div(a, x, y):
1306	  match x y:
1307	    case 0n 0n:
1308	      {==}
1309	    case 0n 1n+yp:
1310	      {==}
1311	    case 1n+xp 0n:
1312	      %Equal.sym(Nat, Nat.mul(1n+xp, 0n), 0n, mul_zero_r(1n+xp)) : {0n == Nat.div(a, _) : Nat}
1313	      {==}
1314	    case 1n+xp 1n+yp:
1315	      +x1 = {1n+xp : Nat}
1316	      +y1 = {1n+yp : Nat}
1317	      +q1 = Nat.div(a, x1)
1318	      +r1 = Nat.mod(a, x1)
1319	      +q2 = Nat.div(q1, y1)
1320	      +r2 = Nat.mod(q1, y1)
1321	      +xy = Nat.mul(x1, y1)
1322	      +s = Nat.add(Nat.mul(r2, x1), r1)
1323	      # a = q2 * (x * y) + (r2 * x + r1)
1324	      +ea = Equal.trans(Nat, Nat.add(Nat.mul(q2, xy), s), Nat.add(Nat.mul(q1, x1), r1), a,
1325	        %div_mod(q1, y1) : {Nat.add(Nat.mul(q2, xy), s) == Nat.add(Nat.mul(_, x1), r1) : Nat}
1326	        %Equal.sym(Nat, Nat.mul(Nat.add(Nat.mul(q2, y1), r2), x1), Nat.add(Nat.mul(Nat.mul(q2, y1), x1), Nat.mul(r2, x1)), mul_add_r(Nat.mul(q2, y1), r2, x1)) :
1327	          {Nat.add(Nat.mul(q2, xy), s) == Nat.add(_, r1) : Nat}
1328	        %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(Nat.mul(q2, y1), x1), Nat.mul(r2, x1)), r1), Nat.add(Nat.mul(Nat.mul(q2, y1), x1), s),
1329	            add_assoc(Nat.mul(Nat.mul(q2, y1), x1), Nat.mul(r2, x1), r1)) : {Nat.add(Nat.mul(q2, xy), s) == _ : Nat}
1330	        %Equal.trans(Nat, Nat.mul(q2, xy), Nat.mul(q2, Nat.mul(y1, x1)), Nat.mul(Nat.mul(q2, y1), x1),
1331	            %mul_comm(x1, y1) : {Nat.mul(q2, xy) == Nat.mul(q2, _) : Nat}; {==},
1332	            Equal.sym(Nat, Nat.mul(Nat.mul(q2, y1), x1), Nat.mul(q2, Nat.mul(y1, x1)), mul_assoc(q2, y1, x1))) :
1333	          {Nat.add(Nat.mul(q2, xy), s) == Nat.add(_, s) : Nat}
1334	        {==},
1335	        div_mod(a, x1))
1336	      # r2 * x + r1 < x * y
1337	      +hs = lt_le_trans(s, Nat.add(Nat.mul(r2, x1), x1), xy,
1338	        lt_add_l(Nat.mul(r2, x1), r1, x1, mod_lt(a, x1, {==})),
1339	        %add_comm(x1, Nat.mul(r2, x1)) : {Nat.is_le(_, xy) == True{} : Bool}
1340	        %mul_comm(y1, x1) : {Nat.is_le(Nat.mul(1n+r2, x1), _) == True{} : Bool}
1341	        le_mul_r(1n+r2, y1, x1, %Equal.sym(Bool, Nat.is_le(1n+r2, y1), Nat.is_lt(r2, y1), le_succ_lt(r2, y1)) : {_ == True{} : Bool}; mod_lt(q1, y1, {==})))
1342	      %ea : {q2 == Nat.div(_, xy) : Nat}
1343	      Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(q2, xy), s), xy), q2, div_mul_add(q2, xy, s, hs))
1344	
1345	# a < b * c with b > 0 gives a / b < c.
1346	def div_lt.go(+a: Nat, +b: Nat, +c: Nat, +h: {Nat.is_lt(a, Nat.mul(b, c)) == True{} : Bool},
1347	  t: Bool, et: {Nat.is_lt(Nat.div(a, b), c) == t : Bool}) -> {Nat.is_lt(Nat.div(a, b), c) == True{} : Bool}:
1348	  match t:
1349	    case True{}:
1350	      et
1351	    case False{}:
1352	      +q = Nat.div(a, b)
1353	      +hcq = not_lt_le(q, c, et)
1354	      +hle = le_trans(Nat.mul(c, b), Nat.mul(q, b), a, le_mul_r(c, q, b, hcq),
1355	        %div_mod(a, b) : {Nat.is_le(Nat.mul(q, b), _) == True{} : Bool}
1356	        le_add_r(Nat.mul(q, b), Nat.mod(a, b)))
1357	      +hlt = lt_le_trans(a, Nat.mul(b, c), a, h, %mul_comm(c, b) : {Nat.is_le(_, a) == True{} : Bool}; hle)
1358	      Empty.absurd({Nat.is_lt(q, c) == True{} : Bool}, false_ne_true(
1359	        Equal.trans(Bool, False{}, Nat.is_lt(a, a), True{}, Equal.sym(Bool, Nat.is_lt(a, a), False{}, lt_irrefl(a)), hlt)))
1360	
1361	law div_lt:
1362	  for +a: Nat
1363	  for +b: Nat
1364	  for +c: Nat
1365	  for +hb: {Nat.is_lt(0n, b) == True{} : Bool}
1366	  for +h: {Nat.is_lt(a, Nat.mul(b, c)) == True{} : Bool}
1367	  {Nat.is_lt(Nat.div(a, b), c) == True{} : Bool}
1368	
1369	def div_lt(a, b, c, hb, h):
1370	  div_lt.go(a, b, c, h, Nat.is_lt(Nat.div(a, b), c), {==})
1371	
1372	# Powers
1373	# ======
1374	
1375	law pow_add:
1376	  for +b: Nat
1377	  for +j: Nat
1378	  for +k: Nat
1379	  {Nat.pow(b, Nat.add(j, k)) == Nat.mul(Nat.pow(b, j), Nat.pow(b, k)) : Nat}
1380	
1381	def pow_add(b, j, k):
1382	  match j:
1383	    case 0n:
1384	      Equal.sym(Nat, Nat.add(Nat.pow(b, k), 0n), Nat.pow(b, k), add_zero(Nat.pow(b, k)))
1385	    case 1n+p:
1386	      %Equal.sym(Nat, Nat.pow(b, Nat.add(p, k)), Nat.mul(Nat.pow(b, p), Nat.pow(b, k)), pow_add(b, p, k)) :
1387	        {Nat.mul(b, _) == Nat.mul(Nat.mul(b, Nat.pow(b, p)), Nat.pow(b, k)) : Nat}
1388	      Equal.sym(Nat, Nat.mul(Nat.mul(b, Nat.pow(b, p)), Nat.pow(b, k)), Nat.mul(b, Nat.mul(Nat.pow(b, p), Nat.pow(b, k))),
1389	        mul_assoc(b, Nat.pow(b, p), Nat.pow(b, k)))
1390	
1391	law pow_pos:
1392	  for +k: Nat
1393	  {Nat.is_lt(0n, Nat.pow(2n, k)) == True{} : Bool}
1394	
1395	def pow_pos(k):
1396	  match k:
1397	    case 0n:
1398	      {==}
1399	    case 1n+j:
1400	      pos_add_l(Nat.pow(2n, j), Nat.mul(1n, Nat.pow(2n, j)), pow_pos(j))
1401	
1402	law pow2s:
1403	  for +p: Nat
1404	  {Nat.pow(2n, 1n+p) == Nat.double(Nat.pow(2n, p)) : Nat}
1405	
1406	def pow2s(p):
1407	  mul2(Nat.pow(2n, p))
1408	
1409	# 2^(1+j) - 1 = 1 + 2 (2^j - 1).
1410	law pow_sub1:
1411	  for +j: Nat
1412	  {Nat.sub(Nat.pow(2n, 1n+j), 1n) == 1n+Nat.double(Nat.sub(Nat.pow(2n, j), 1n)) : Nat}
1413	
1414	def pow_sub1.go(+u: Nat) -> {Nat.sub(Nat.double(1n+u), 1n) == 1n+Nat.double(Nat.sub(1n+u, 1n)) : Nat}:
1415	  %Equal.sym(Nat, Nat.sub(u, 0n), u, sub_zero(u)) : {Nat.sub(Nat.double(1n+u), 1n) == 1n+Nat.double(_) : Nat}
1416	  {==}
1417	
1418	law pow_one_plus:
1419	  for +k: Nat
1420	  {1n+Nat.sub(Nat.pow(2n, k), 1n) == Nat.pow(2n, k) : Nat}
1421	
1422	def pow_one_plus(k):
1423	  match k:
1424	    case 0n:
1425	      {==}
1426	    case 1n+j:
1427	      %Equal.sym(Nat, Nat.mul(2n, Nat.pow(2n, j)), Nat.double(Nat.pow(2n, j)), mul2(Nat.pow(2n, j))) :
1428	        {1n+Nat.sub(_, 1n) == _ : Nat}
1429	      %pow_one_plus(j) : {1n+Nat.sub(Nat.double(_), 1n) == Nat.double(_) : Nat}
1430	      {==}
1431	
1432	def pow_sub1(j):
1433	  %Equal.sym(Nat, Nat.mul(2n, Nat.pow(2n, j)), Nat.double(Nat.pow(2n, j)), mul2(Nat.pow(2n, j))) :
1434	    {Nat.sub(_, 1n) == 1n+Nat.double(Nat.sub(Nat.pow(2n, j), 1n)) : Nat}
1435	  %pow_one_plus(j) : {Nat.sub(Nat.double(_), 1n) == 1n+Nat.double(Nat.sub(_, 1n)) : Nat}
1436	  pow_sub1.go(Nat.sub(Nat.pow(2n, j), 1n))
1437	
1438	# 2^m <= 2^k for m <= k.
1439	law pow_le:
1440	  for +m: Nat
1441	  for +k: Nat
1442	  for +h: {Nat.is_le(m, k) == True{} : Bool}
1443	  {Nat.is_le(Nat.pow(2n, m), Nat.pow(2n, k)) == True{} : Bool}
1444	
1445	def pow_le(m, k, h):
1446	  %le_sub_add(m, k, h) : {Nat.is_le(Nat.pow(2n, m), Nat.pow(2n, _)) == True{} : Bool}
1447	  %Equal.sym(Nat, Nat.pow(2n, Nat.add(m, Nat.sub(k, m))), Nat.mul(Nat.pow(2n, m), Nat.pow(2n, Nat.sub(k, m))), pow_add(2n, m, Nat.sub(k, m))) :
1448	    {Nat.is_le(Nat.pow(2n, m), _) == True{} : Bool}
1449	  %mul_one(Nat.pow(2n, m)) :
1450	    {Nat.is_le(_, Nat.mul(Nat.pow(2n, m), Nat.pow(2n, Nat.sub(k, m)))) == True{} : Bool}
1451	  le_mul_l(Nat.pow(2n, m), 1n, Nat.pow(2n, Nat.sub(k, m)),
1452	    %Equal.sym(Bool, Nat.is_le(1n, Nat.pow(2n, Nat.sub(k, m))), Nat.is_lt(0n, Nat.pow(2n, Nat.sub(k, m))), le_succ_lt(0n, Nat.pow(2n, Nat.sub(k, m)))) : {_ == True{} : Bool}
1453	    pow_pos(Nat.sub(k, m)))
1454	
1455	# (a % 2^m) % 2^k = a % 2^k for k <= m.
1456	law mod_mod_pow:
1457	  for +a: Nat
1458	  for +k: Nat
1459	  for +m: Nat
1460	  for +h: {Nat.is_le(k, m) == True{} : Bool}
1461	  {Nat.mod(Nat.mod(a, Nat.pow(2n, m)), Nat.pow(2n, k)) == Nat.mod(a, Nat.pow(2n, k)) : Nat}
1462	
1463	def mod_mod_pow(a, k, m, h):
1464	  %le_sub_add(k, m, h) : {Nat.mod(Nat.mod(a, Nat.pow(2n, _)), Nat.pow(2n, k)) == Nat.mod(a, Nat.pow(2n, k)) : Nat}
1465	  %Equal.sym(Nat, Nat.pow(2n, Nat.add(k, Nat.sub(m, k))), Nat.mul(Nat.pow(2n, k), Nat.pow(2n, Nat.sub(m, k))), pow_add(2n, k, Nat.sub(m, k))) :
1466	    {Nat.mod(Nat.mod(a, _), Nat.pow(2n, k)) == Nat.mod(a, Nat.pow(2n, k)) : Nat}
1467	  mod_mod_mul(a, Nat.pow(2n, k), Nat.pow(2n, Nat.sub(m, k)))
1468	
1469	# m <= k + (m - k).
1470	law le_add_sub:
1471	  for +m: Nat
1472	  for +k: Nat
1473	  {Nat.is_le(m, Nat.add(k, Nat.sub(m, k))) == True{} : Bool}
1474	
1475	def le_add_sub(m, k):
1476	  match m k:
1477	    case 0n _:
1478	      le_zero_l(Nat.add(k, Nat.sub(0n, k)))
1479	    case 1n+p 0n:
1480	      le_refl(1n+p)
1481	    case 1n+p 1n+q:
1482	      le_add_sub(p, q)
1483	
1484	law eq_comm:
1485	  for +a: Nat
1486	  for +b: Nat
1487	  {Nat.is_eq(a, b) == Nat.is_eq(b, a) : Bool}
1488	
1489	def eq_comm(a, b):
1490	  match a b:
1491	    case 0n 0n:
1492	      {==}
1493	    case 0n 1n+q:
1494	      {==}
1495	    case 1n+p 0n:
1496	      {==}
1497	    case 1n+p 1n+q:
1498	      eq_comm(p, q)
1499	
1500	# a <= b and a != b give a + 1 <= b.
1501	law le_ne:
1502	  for +a: Nat
1503	  for +b: Nat
1504	  for +le: {Nat.is_le(a, b) == True{} : Bool}
1505	  for +ne: {Nat.is_eq(a, b) == False{} : Bool}
1506	  {Nat.is_le(1n+a, b) == True{} : Bool}
1507	
1508	def le_ne(a, b, le, ne):
1509	  match a b:
1510	    case 0n 0n:
1511	      Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, true_ne_false(ne))
1512	    case 0n 1n+q:
1513	      le_zero_l(q)
1514	    case 1n+p 0n:
1515	      Empty.absurd({Nat.is_le(2n+p, 0n) == True{} : Bool}, false_ne_true(le))
1516	    case 1n+p 1n+q:
1517	      le_ne(p, q, le, ne)
1518	
1519	# a <= b gives not (b < a).
1520	law le_not_lt:
1521	  for +a: Nat
1522	  for +b: Nat
1523	  for +h: {Nat.is_le(a, b) == True{} : Bool}
1524	  {Nat.is_lt(b, a) == False{} : Bool}
1525	
1526	def le_not_lt(a, b, h):
1527	  match a b:
1528	    case 0n _:
1529	      lt_zero(b)
1530	    case 1n+p 0n:
1531	      Empty.absurd({Nat.is_lt(0n, 1n+p) == False{} : Bool}, false_ne_true(h))
1532	    case 1n+p 1n+q:
1533	      le_not_lt(p, q, h)
1534	
1535	# a + c <= x gives c <= x - a.
1536	law le_sub_r:
1537	  for +a: Nat
1538	  for +c: Nat
1539	  for +x: Nat
1540	  for +h: {Nat.is_le(Nat.add(a, c), x) == True{} : Bool}
1541	  {Nat.is_le(c, Nat.sub(x, a)) == True{} : Bool}
1542	
1543	def le_sub_r(a, c, x, h):
1544	  match a x:
1545	    case 0n _:
1546	      %Equal.sym(Nat, Nat.sub(x, 0n), x, sub_zero(x)) : {Nat.is_le(c, _) == True{} : Bool}
1547	      h
1548	    case 1n+p 0n:
1549	      Empty.absurd({Nat.is_le(c, Nat.sub(0n, 1n+p)) == True{} : Bool}, false_ne_true(h))
1550	    case 1n+p 1n+y:
1551	      le_sub_r(p, c, y, h)
1552	
1553	# 8a < 8b gives a < b.
1554	def lt_mul_cancel.go(+c: Nat, +a: Nat, +b: Nat, +h: {Nat.is_lt(Nat.mul(c, a), Nat.mul(c, b)) == True{} : Bool},
1555	  t: Bool, et: {Nat.is_lt(a, b) == t : Bool}) -> {Nat.is_lt(a, b) == True{} : Bool}:
1556	  match t:
1557	    case True{}:
1558	      et
1559	    case False{}:
1560	      Empty.absurd({Nat.is_lt(a, b) == True{} : Bool}, false_ne_true(
1561	        Equal.trans(Bool, False{}, Nat.is_lt(Nat.mul(c, a), Nat.mul(c, a)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.mul(c, a), Nat.mul(c, a)), False{}, lt_irrefl(Nat.mul(c, a))),
1562	          lt_le_trans(Nat.mul(c, a), Nat.mul(c, b), Nat.mul(c, a), h, le_mul_l(c, b, a, not_lt_le(a, b, et))))))
1563	
1564	law lt_mul_cancel:
1565	  for +c: Nat
1566	  for +a: Nat
1567	  for +b: Nat
1568	  for +h: {Nat.is_lt(Nat.mul(c, a), Nat.mul(c, b)) == True{} : Bool}
1569	  {Nat.is_lt(a, b) == True{} : Bool}
1570	
1571	def lt_mul_cancel(c, a, b, h):
1572	  lt_mul_cancel.go(c, a, b, h, Nat.is_lt(a, b), {==})