1	# bend-mathlib/nat.bend: Nat arithmetic (add, mul, sub, div, mod, min, max, pow, double) and order
2	# (le, lt, ge, gt).
3	import Base
4	
5	# Zero is a right identity for addition: x + 0 = x.
6	law add_zero:
7	  for x: Nat
8	  {Nat.add(x, 0n) == x : Nat}
9	
10	def add_zero(x):
11	  match x:
12	    case 0n:
13	      {==}
14	    case 1n+p:
15	      %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
16	      {==}
17	
18	# Zero is a left identity for addition: 0 + x = x.
19	law zero_add:
20	  for -x: Nat
21	  {Nat.add(0n, x) == x : Nat}
22	
23	def zero_add(x):
24	  {==}
25	
26	# Adding a successor on the right: n + (m + 1) = (n + m) + 1.
27	law add_succ:
28	  for n: Nat
29	  for -m: Nat
30	  {Nat.add(n, 1n+m) == 1n+Nat.add(n, m) : Nat}
31	
32	def add_succ(n, m):
33	  match n:
34	    case 0n:
35	      {==}
36	    case 1n+p:
37	      %add_succ(p, m) : {1n+Nat.add(p, 1n+m) == 1n+_ : Nat}
38	      {==}
39	
40	# Adding a successor on the left: (n + 1) + m = (n + m) + 1.
41	law succ_add:
42	  for -n: Nat
43	  for -m: Nat
44	  {Nat.add(1n+n, m) == 1n+Nat.add(n, m) : Nat}
45	
46	def succ_add(n, m):
47	  {==}
48	
49	# Addition is commutative: n + m = m + n.
50	law add_comm:
51	  for n: Nat
52	  for m: Nat
53	  {Nat.add(n, m) == Nat.add(m, n) : Nat}
54	
55	def add_comm(n, m):
56	  match n m:
57	    case 0n 0n:
58	      {==}
59	    case 0n 1n+q:
60	      %add_zero(q) : {1n+_ == 1n+Nat.add(q, 0n) : Nat}
61	      {==}
62	    case 1n+p 0n:
63	      %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
64	      {==}
65	    case 1n++p 1n++q:
66	      %Equal.sym(Nat, Nat.add(p, 1n+q), 1n+Nat.add(p, q), add_succ(p, q)) : {1n+_ == 1n+Nat.add(q, 1n+p) : Nat}
67	      %Equal.sym(Nat, Nat.add(q, 1n+p), 1n+Nat.add(q, p), add_succ(q, p)) : {2n+Nat.add(p, q) == 1n+_ : Nat}
68	      %add_comm(p, q) : {2n+Nat.add(p, q) == 2n+_ : Nat}
69	      {==}
70	
71	# Addition is associative: (a + b) + c = a + (b + c).
72	law add_assoc:
73	  for a: Nat
74	  for -b: Nat
75	  for -c: Nat
76	  {Nat.add(Nat.add(a, b), c) == Nat.add(a, Nat.add(b, c)) : Nat}
77	
78	def add_assoc(a, b, c):
79	  match a:
80	    case 0n:
81	      {==}
82	    case 1n+p:
83	      %add_assoc(p, b, c) : {1n+Nat.add(Nat.add(p, b), c) == 1n+_ : Nat}
84	      {==}
85	
86	# Left commutativity of addition: a + (b + c) = b + (a + c).
87	law add_left_comm:
88	  for a: Nat
89	  for b: Nat
90	  for -c: Nat
91	  {Nat.add(a, Nat.add(b, c)) == Nat.add(b, Nat.add(a, c)) : Nat}
92	
93	def add_left_comm(a, b, c):
94	  match a:
95	    case 0n:
96	      {==}
97	    case 1n+p:
98	      +b = b
99	      %Equal.sym(Nat, Nat.add(b, 1n+Nat.add(p, c)), 1n+Nat.add(b, Nat.add(p, c)), add_succ(b, Nat.add(p, c))) : {1n+Nat.add(p, Nat.add(b, c)) == _ : Nat}
100	      %add_left_comm(p, b, c) : {1n+Nat.add(p, Nat.add(b, c)) == 1n+_ : Nat}
101	      {==}
102	
103	# Right commutativity of addition: (a + b) + c = (a + c) + b.
104	law add_right_comm:
105	  for a: Nat
106	  for b: Nat
107	  for c: Nat
108	  {Nat.add(Nat.add(a, b), c) == Nat.add(Nat.add(a, c), b) : Nat}
109	
110	def add_right_comm(a, b, c):
111	  match a:
112	    case 0n:
113	      add_comm(b, c)
114	    case 1n+p:
115	      %add_right_comm(p, b, c) : {1n+Nat.add(Nat.add(p, b), c) == 1n+_ : Nat}
116	      {==}
117	
118	# Four-way regrouping of a sum: (a + b) + (c + d) = (a + c) + (b + d).
119	law add_add_add_comm:
120	  for a: Nat
121	  for b: Nat
122	  for c: Nat
123	  for -d: Nat
124	  {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}
125	
126	def add_add_add_comm(a, b, c, d):
127	  match a:
128	    case 0n:
129	      add_left_comm(b, c, d)
130	    case 1n+p:
131	      %add_add_add_comm(p, b, c, d) : {1n+Nat.add(Nat.add(p, b), Nat.add(c, d)) == 1n+_ : Nat}
132	      {==}
133	
134	def internal_pred(n: Nat) -> Nat:
135	  match n:
136	    case 0n:
137	      0n
138	    case 1n+p:
139	      p
140	
141	# The successor function is injective: a + 1 = b + 1 implies a = b.
142	law succ_inj:
143	  for -a: Nat
144	  for -b: Nat
145	  for e: {1n+a == 1n+b : Nat}
146	  {a == b : Nat}
147	
148	def succ_inj(a, b, e):
149	  %e : {a == internal_pred(_) : Nat}
150	  {==}
151	
152	def internal_zero_ne_succ(-n: Nat, e: {0n == 1n+n : Nat}) -> Empty:
153	  %e : Bool.pick(Type, Nat.is_eq(_, 0n), Unit, Empty)
154	  Unit{}
155	
156	# Zero is not a successor.
157	law zero_ne_succ:
158	  for -n: Nat
159	  {0n != 1n+n : Nat}
160	
161	def zero_ne_succ(n):
162	  e => internal_zero_ne_succ(n, e)
163	
164	def internal_succ_ne_zero(-n: Nat, e: {1n+n == 0n : Nat}) -> Empty:
165	  %e : Bool.pick(Type, Nat.is_eq(_, 0n), Empty, Unit)
166	  Unit{}
167	
168	# A successor is not zero.
169	law succ_ne_zero:
170	  for -n: Nat
171	  {1n+n != 0n : Nat}
172	
173	def succ_ne_zero(n):
174	  e => internal_succ_ne_zero(n, e)
175	
176	# Addition cancels on the left: a + b = a + c implies b = c.
177	law add_left_cancel:
178	  for a: Nat
179	  for -b: Nat
180	  for -c: Nat
181	  for e: {Nat.add(a, b) == Nat.add(a, c) : Nat}
182	  {b == c : Nat}
183	
184	def add_left_cancel(a, b, c, e):
185	  match a:
186	    case 0n:
187	      e
188	    case 1n+p:
189	      add_left_cancel(p, b, c, succ_inj(Nat.add(p, b), Nat.add(p, c), e))
190	
191	# Addition cancels on the right: a + b = c + b implies a = c.
192	law add_right_cancel:
193	  for a: Nat
194	  for b: Nat
195	  for c: Nat
196	  for e: {Nat.add(a, b) == Nat.add(c, b) : Nat}
197	  {a == c : Nat}
198	
199	def add_right_cancel(a, b, c, e):
200	  +b = b
201	  add_left_cancel(b, a, c, Equal.trans(Nat, Nat.add(b, a), Nat.add(a, b), Nat.add(b, c), add_comm(b, a), Equal.trans(Nat, Nat.add(a, b), Nat.add(c, b), Nat.add(b, c), e, add_comm(c, b))))
202	
203	# Zero absorbs multiplication on the right: x * 0 = 0.
204	law mul_zero:
205	  for x: Nat
206	  {Nat.mul(x, 0n) == 0n : Nat}
207	
208	def mul_zero(x):
209	  match x:
210	    case 0n:
211	      {==}
212	    case 1n+p:
213	      mul_zero(p)
214	
215	# Zero absorbs multiplication on the left: 0 * x = 0.
216	law zero_mul:
217	  for -x: Nat
218	  {Nat.mul(0n, x) == 0n : Nat}
219	
220	def zero_mul(x):
221	  {==}
222	
223	# One is a right identity for multiplication: x * 1 = x.
224	law mul_one:
225	  for x: Nat
226	  {Nat.mul(x, 1n) == x : Nat}
227	
228	def mul_one(x):
229	  match x:
230	    case 0n:
231	      {==}
232	    case 1n+p:
233	      %mul_one(p) : {1n+Nat.mul(p, 1n) == 1n+_ : Nat}
234	      {==}
235	
236	# One is a left identity for multiplication: 1 * x = x.
237	law one_mul:
238	  for x: Nat
239	  {Nat.mul(1n, x) == x : Nat}
240	
241	def one_mul(x):
242	  add_zero(x)
243	
244	# Multiplying by a successor on the right: n * (m + 1) = n * m + n.
245	law mul_succ:
246	  for n: Nat
247	  for m: Nat
248	  {Nat.mul(n, 1n+m) == Nat.add(Nat.mul(n, m), n) : Nat}
249	
250	def mul_succ(n, m):
251	  match n:
252	    case 0n:
253	      {==}
254	    case 1n++p:
255	      +m = m
256	      %Equal.sym(Nat, Nat.add(Nat.add(m, Nat.mul(p, m)), 1n+p), 1n+Nat.add(Nat.add(m, Nat.mul(p, m)), p), add_succ(Nat.add(m, Nat.mul(p, m)), p)) : {1n+Nat.add(m, Nat.mul(p, 1n+m)) == _ : Nat}
257	      %Equal.sym(Nat, Nat.add(Nat.add(m, Nat.mul(p, m)), p), Nat.add(m, Nat.add(Nat.mul(p, m), p)), add_assoc(m, Nat.mul(p, m), p)) : {1n+Nat.add(m, Nat.mul(p, 1n+m)) == 1n+_ : Nat}
258	      %mul_succ(p, m) : {1n+Nat.add(m, Nat.mul(p, 1n+m)) == 1n+Nat.add(m, _) : Nat}
259	      {==}
260	
261	# Multiplying by a successor on the left: (n + 1) * m = n * m + m.
262	law succ_mul:
263	  for n: Nat
264	  for m: Nat
265	  {Nat.mul(1n+n, m) == Nat.add(Nat.mul(n, m), m) : Nat}
266	
267	def succ_mul(n, m):
268	  +m = m
269	  add_comm(m, Nat.mul(n, m))
270	
271	# Multiplication is commutative: n * m = m * n.
272	law mul_comm:
273	  for n: Nat
274	  for m: Nat
275	  {Nat.mul(n, m) == Nat.mul(m, n) : Nat}
276	
277	def mul_comm(n, m):
278	  match n:
279	    case 0n:
280	      %mul_zero(m) : {_ == Nat.mul(m, 0n) : Nat}
281	      {==}
282	    case 1n++p:
283	      +m = m
284	      %Equal.sym(Nat, Nat.mul(m, 1n+p), Nat.add(Nat.mul(m, p), m), mul_succ(m, p)) : {Nat.add(m, Nat.mul(p, m)) == _ : Nat}
285	      %mul_comm(p, m) : {Nat.add(m, Nat.mul(p, m)) == Nat.add(_, m) : Nat}
286	      add_comm(m, Nat.mul(p, m))
287	
288	# Multiplication distributes over addition on the right: (a + b) * c = a * c + b * c.
289	law add_mul:
290	  for a: Nat
291	  for -b: Nat
292	  for c: Nat
293	  {Nat.mul(Nat.add(a, b), c) == Nat.add(Nat.mul(a, c), Nat.mul(b, c)) : Nat}
294	
295	def add_mul(a, b, c):
296	  match a:
297	    case 0n:
298	      {==}
299	    case 1n+p:
300	      +c = c
301	      %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))), add_assoc(c, Nat.mul(p, c), Nat.mul(b, c))) : {Nat.add(c, Nat.mul(Nat.add(p, b), c)) == _ : Nat}
302	      %add_mul(p, b, c) : {Nat.add(c, Nat.mul(Nat.add(p, b), c)) == Nat.add(c, _) : Nat}
303	      {==}
304	
305	# Multiplication distributes over addition on the left: a * (b + c) = a * b + a * c.
306	law mul_add:
307	  for a: Nat
308	  for b: Nat
309	  for c: Nat
310	  {Nat.mul(a, Nat.add(b, c)) == Nat.add(Nat.mul(a, b), Nat.mul(a, c)) : Nat}
311	
312	def mul_add(a, b, c):
313	  match a:
314	    case 0n:
315	      {==}
316	    case 1n++p:
317	      +b = b
318	      +c = c
319	      %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}
320	      add_add_add_comm(b, c, Nat.mul(p, b), Nat.mul(p, c))
321	
322	# Multiplication is associative: (a * b) * c = a * (b * c).
323	law mul_assoc:
324	  for a: Nat
325	  for b: Nat
326	  for c: Nat
327	  {Nat.mul(Nat.mul(a, b), c) == Nat.mul(a, Nat.mul(b, c)) : Nat}
328	
329	def mul_assoc(a, b, c):
330	  match a:
331	    case 0n:
332	      {==}
333	    case 1n+p:
334	      +b = b
335	      +c = c
336	      %mul_assoc(p, b, c) : {Nat.mul(Nat.add(b, Nat.mul(p, b)), c) == Nat.add(Nat.mul(b, c), _) : Nat}
337	      add_mul(b, Nat.mul(p, b), c)
338	
339	# The order a <= b on naturals, as a reusable proposition.
340	def le(a: Nat, b: Nat) -> Data:
341	  {Nat.is_le(a, b) == True{} : Bool}
342	
343	# The strict order a < b on naturals, as a reusable proposition.
344	def lt(a: Nat, b: Nat) -> Data:
345	  {Nat.is_lt(a, b) == True{} : Bool}
346	
347	# The order a >= b on naturals, as a reusable proposition.
348	def ge(a: Nat, b: Nat) -> Data:
349	  {Nat.is_ge(a, b) == True{} : Bool}
350	
351	# The strict order a > b on naturals, as a reusable proposition.
352	def gt(a: Nat, b: Nat) -> Data:
353	  {Nat.is_gt(a, b) == True{} : Bool}
354	
355	def internal_false_ne_true(e: {False{} == True{} : Bool}) -> Empty:
356	  %e : Bool.pick(Type, _, Empty, Unit)
357	  Unit{}
358	
359	# Every natural is at most itself: a <= a.
360	law le_refl:
361	  for a: Nat
362	  le(a, a)
363	
364	def le_refl(a):
365	  match a:
366	    case 0n:
367	      {==}
368	    case 1n+p:
369	      le_refl(p)
370	
371	# Zero is at most every natural: 0 <= b.
372	law zero_le:
373	  for b: Nat
374	  le(0n, b)
375	
376	def zero_le(b):
377	  match b:
378	    case 0n:
379	      {==}
380	    case 1n+p:
381	      {==}
382	
383	# Every natural is at most its successor: n <= n + 1.
384	law le_succ:
385	  for n: Nat
386	  le(n, 1n+n)
387	
388	def le_succ(n):
389	  match n:
390	    case 0n:
391	      {==}
392	    case 1n+p:
393	      le_succ(p)
394	
395	# Adding on the right never decreases a natural: n <= n + k.
396	law le_add_right:
397	  for n: Nat
398	  for k: Nat
399	  le(n, Nat.add(n, k))
400	
401	def le_add_right(n, k):
402	  match n:
403	    case 0n:
404	      zero_le(k)
405	    case 1n+p:
406	      le_add_right(p, k)
407	
408	# The order is transitive: a <= b and b <= c imply a <= c.
409	law le_trans:
410	  for a: Nat
411	  for b: Nat
412	  for c: Nat
413	  for ab: le(a, b)
414	  for bc: le(b, c)
415	  le(a, c)
416	
417	def le_trans(a, b, c, ab, bc):
418	  match a b c:
419	    case 0n _ 0n:
420	      {==}
421	    case 0n _ 1n+r:
422	      {==}
423	    case 1n+p 0n _:
424	      Empty.absurd(le(1n+p, c), internal_false_ne_true(ab))
425	    case 1n+p 1n+q 0n:
426	      Empty.absurd(le(1n+p, 0n), internal_false_ne_true(bc))
427	    case 1n+p 1n+q 1n+r:
428	      le_trans(p, q, r, ab, bc)
429	
430	# The order is antisymmetric: a <= b and b <= a imply a = b.
431	law le_antisymm:
432	  for a: Nat
433	  for b: Nat
434	  for ab: le(a, b)
435	  for ba: le(b, a)
436	  {a == b : Nat}
437	
438	def le_antisymm(a, b, ab, ba):
439	  match a b:
440	    case 0n 0n:
441	      {==}
442	    case 0n 1n+q:
443	      Empty.absurd({0n == 1n+q : Nat}, internal_false_ne_true(ba))
444	    case 1n+p 0n:
445	      Empty.absurd({1n+p == 0n : Nat}, internal_false_ne_true(ab))
446	    case 1n+p 1n+q:
447	      %le_antisymm(p, q, ab, ba) : {1n+p == 1n+_ : Nat}
448	      {==}
449	
450	# The order is total: a <= b or b <= a.
451	law le_total:
452	  for a: Nat
453	  for b: Nat
454	  Or(le(a, b), le(b, a))
455	
456	def le_total(a, b):
457	  match a b:
458	    case 0n 0n:
459	      Inl{{==}}
460	    case 0n 1n+q:
461	      Inl{{==}}
462	    case 1n+p 0n:
463	      Inr{{==}}
464	    case 1n+p 1n+q:
465	      le_total(p, q)
466	
467	# The order is total, as a reusable sum: a <= b or b <= a.
468	law le_total_d:
469	  for a: Nat
470	  for b: Nat
471	  Either<&2, &2, le(a, b), le(b, a)>
472	
473	def le_total_d(a, b):
474	  match a b:
475	    case 0n 0n:
476	      Inl{{==}}
477	    case 0n 1n+q:
478	      Inl{{==}}
479	    case 1n+p 0n:
480	      Inr{{==}}
481	    case 1n+p 1n+q:
482	      le_total_d(p, q)
483	
484	# No natural is less than itself.
485	law lt_irrefl:
486	  for a: Nat
487	  lt(a, a) -> Empty
488	
489	def lt_irrefl(a):
490	  match a:
491	    case 0n:
492	      h => internal_false_ne_true(h)
493	    case 1n+p:
494	      lt_irrefl(p)
495	
496	# The strict order is transitive: a < b and b < c imply a < c.
497	law lt_trans:
498	  for a: Nat
499	  for b: Nat
500	  for c: Nat
501	  for ab: lt(a, b)
502	  for bc: lt(b, c)
503	  lt(a, c)
504	
505	def lt_trans(a, b, c, ab, bc):
506	  match a b c:
507	    case 0n 0n _:
508	      Empty.absurd(lt(0n, c), internal_false_ne_true(ab))
509	    case 0n 1n+q 0n:
510	      Empty.absurd(lt(0n, 0n), internal_false_ne_true(bc))
511	    case 0n 1n+q 1n+r:
512	      {==}
513	    case 1n+p 0n _:
514	      Empty.absurd(lt(1n+p, c), internal_false_ne_true(ab))
515	    case 1n+p 1n+q 0n:
516	      Empty.absurd(lt(1n+p, 0n), internal_false_ne_true(bc))
517	    case 1n+p 1n+q 1n+r:
518	      lt_trans(p, q, r, ab, bc)
519	
520	# A strict inequality implies the weak one: a < b implies a <= b.
521	law le_of_lt:
522	  for a: Nat
523	  for b: Nat
524	  for h: lt(a, b)
525	  le(a, b)
526	
527	def le_of_lt(a, b, h):
528	  match a b:
529	    case 0n 0n:
530	      {==}
531	    case 0n 1n+q:
532	      {==}
533	    case 1n+p 0n:
534	      Empty.absurd(le(1n+p, 0n), internal_false_ne_true(h))
535	    case 1n+p 1n+q:
536	      le_of_lt(p, q, h)
537	
538	# Flipping a >= b gives b <= a.
539	law le_of_ge:
540	  for a: Nat
541	  for b: Nat
542	  for h: ge(a, b)
543	  le(b, a)
544	
545	def le_of_ge(a, b, h):
546	  match a b:
547	    case 0n 0n:
548	      {==}
549	    case 0n 1n+q:
550	      Empty.absurd(le(1n+q, 0n), internal_false_ne_true(h))
551	    case 1n+p 0n:
552	      {==}
553	    case 1n+p 1n+q:
554	      le_of_ge(p, q, h)
555	
556	# Flipping b <= a gives a >= b.
557	law ge_of_le:
558	  for a: Nat
559	  for b: Nat
560	  for h: le(b, a)
561	  ge(a, b)
562	
563	def ge_of_le(a, b, h):
564	  match a b:
565	    case 0n 0n:
566	      {==}
567	    case 0n 1n+q:
568	      Empty.absurd(ge(0n, 1n+q), internal_false_ne_true(h))
569	    case 1n+p 0n:
570	      {==}
571	    case 1n+p 1n+q:
572	      ge_of_le(p, q, h)
573	
574	# Flipping a > b gives b < a.
575	law lt_of_gt:
576	  for a: Nat
577	  for b: Nat
578	  for h: gt(a, b)
579	  lt(b, a)
580	
581	def lt_of_gt(a, b, h):
582	  match a b:
583	    case 0n 0n:
584	      Empty.absurd(lt(0n, 0n), internal_false_ne_true(h))
585	    case 0n 1n+q:
586	      Empty.absurd(lt(1n+q, 0n), internal_false_ne_true(h))
587	    case 1n+p 0n:
588	      {==}
589	    case 1n+p 1n+q:
590	      lt_of_gt(p, q, h)
591	
592	# Flipping b < a gives a > b.
593	law gt_of_lt:
594	  for a: Nat
595	  for b: Nat
596	  for h: lt(b, a)
597	  gt(a, b)
598	
599	def gt_of_lt(a, b, h):
600	  match a b:
601	    case 0n 0n:
602	      Empty.absurd(gt(0n, 0n), internal_false_ne_true(h))
603	    case 0n 1n+q:
604	      Empty.absurd(gt(0n, 1n+q), internal_false_ne_true(h))
605	    case 1n+p 0n:
606	      {==}
607	    case 1n+p 1n+q:
608	      gt_of_lt(p, q, h)
609	
610	# Subtracting zero changes nothing: n - 0 = n.
611	law sub_zero:
612	  for n: Nat
613	  {Nat.sub(n, 0n) == n : Nat}
614	
615	def sub_zero(n):
616	  match n:
617	    case 0n:
618	      {==}
619	    case 1n+p:
620	      {==}
621	
622	# Truncated subtraction from zero is zero: 0 - n = 0.
623	law zero_sub:
624	  for n: Nat
625	  {Nat.sub(0n, n) == 0n : Nat}
626	
627	def zero_sub(n):
628	  match n:
629	    case 0n:
630	      {==}
631	    case 1n+p:
632	      {==}
633	
634	# A natural minus itself is zero: n - n = 0.
635	law sub_self:
636	  for n: Nat
637	  {Nat.sub(n, n) == 0n : Nat}
638	
639	def sub_self(n):
640	  match n:
641	    case 0n:
642	      {==}
643	    case 1n+p:
644	      sub_self(p)
645	
646	# Subtracting successors: (n + 1) - (m + 1) = n - m.
647	law succ_sub_succ:
648	  for -n: Nat
649	  for -m: Nat
650	  {Nat.sub(1n+n, 1n+m) == Nat.sub(n, m) : Nat}
651	
652	def succ_sub_succ(n, m):
653	  {==}
654	
655	# Adding then subtracting m cancels: (n + m) - m = n.
656	law add_sub_cancel:
657	  for n: Nat
658	  for m: Nat
659	  {Nat.sub(Nat.add(n, m), m) == n : Nat}
660	
661	def add_sub_cancel(n, m):
662	  match m:
663	    case 0n:
664	      +n = n
665	      %Equal.sym(Nat, Nat.add(n, 0n), n, add_zero(n)) : {Nat.sub(_, 0n) == n : Nat}
666	      sub_zero(n)
667	    case 1n++q:
668	      +n = n
669	      %Equal.sym(Nat, Nat.add(n, 1n+q), 1n+Nat.add(n, q), add_succ(n, q)) : {Nat.sub(_, 1n+q) == n : Nat}
670	      add_sub_cancel(n, q)
671	
672	# Adding then subtracting n cancels: (n + m) - n = m.
673	law add_sub_cancel_left:
674	  for n: Nat
675	  for m: Nat
676	  {Nat.sub(Nat.add(n, m), n) == m : Nat}
677	
678	def add_sub_cancel_left(n, m):
679	  match n:
680	    case 0n:
681	      sub_zero(m)
682	    case 1n+p:
683	      add_sub_cancel_left(p, m)
684	
685	# If m <= n, subtracting and adding m back gives n: (n - m) + m = n.
686	law sub_add_cancel:
687	  for n: Nat
688	  for m: Nat
689	  for h: le(m, n)
690	  {Nat.add(Nat.sub(n, m), m) == n : Nat}
691	
692	def sub_add_cancel(n, m, h):
693	  match n m:
694	    case 0n 0n:
695	      {==}
696	    case 0n 1n+q:
697	      Empty.absurd({1n+q == 0n : Nat}, internal_false_ne_true(h))
698	    case 1n++p 0n:
699	      %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
700	      {==}
701	    case 1n++p 1n++q:
702	      %Equal.sym(Nat, Nat.add(Nat.sub(p, q), 1n+q), 1n+Nat.add(Nat.sub(p, q), q), add_succ(Nat.sub(p, q), q)) : {_ == 1n+p : Nat}
703	      %Equal.sym(Nat, Nat.add(Nat.sub(p, q), q), p, sub_add_cancel(p, q, h)) : {1n+_ == 1n+p : Nat}
704	      {==}
705	
706	# Subtracting twice is subtracting the sum: (n - m) - k = n - (m + k).
707	law sub_sub:
708	  for n: Nat
709	  for m: Nat
710	  for k: Nat
711	  {Nat.sub(Nat.sub(n, m), k) == Nat.sub(n, Nat.add(m, k)) : Nat}
712	
713	def sub_sub(n, m, k):
714	  match n m:
715	    case 0n 0n:
716	      {==}
717	    case 0n 1n+q:
718	      zero_sub(k)
719	    case 1n+p 0n:
720	      {==}
721	    case 1n+p 1n+q:
722	      sub_sub(p, q, k)
723	
724	# Truncated subtraction never increases: n - m <= n.
725	law sub_le:
726	  for n: Nat
727	  for m: Nat
728	  le(Nat.sub(n, m), n)
729	
730	def sub_le(n, m):
731	  match n m:
732	    case 0n 0n:
733	      {==}
734	    case 0n 1n+q:
735	      {==}
736	    case 1n+p 0n:
737	      le_refl(1n+p)
738	    case 1n++p 1n++q:
739	      le_trans(Nat.sub(p, q), p, 1n+p, sub_le(p, q), le_succ(p))
740	
741	def internal_div_true_ne_false(h: {True{} == False{} : Bool}) -> Empty:
742	  internal_false_ne_true(Equal.sym(Bool, True{}, False{}, h))
743	
744	def internal_div_add_zero_r(a: Nat) -> {a == Nat.add(a, 0n) : Nat}:
745	  Equal.sym(Nat, Nat.add(a, 0n), a, add_zero(a))
746	
747	def internal_div_le_refl(a: Nat) -> {True{} == Nat.is_le(a, a) : Bool}:
748	  Equal.sym(Bool, Nat.is_le(a, a), True{}, le_refl(a))
749	
750	def internal_div_zero_le(x: Nat) -> {True{} == Nat.is_le(0n, x) : Bool}:
751	  Equal.sym(Bool, Nat.is_le(0n, x), True{}, zero_le(x))
752	
753	def internal_div_block_start(-bp: Nat, +r: Nat, h: {bp == Nat.add(r, 0n) : Nat}) -> {bp == r : Nat}:
754	  %add_zero(r) : {bp == _ : Nat}
755	  h
756	
757	def internal_div_block_step(-bp: Nat, r: Nat, -mp: Nat, h: {bp == Nat.add(r, 1n+mp) : Nat}) -> {bp == 1n+Nat.add(r, mp) : Nat}:
758	  %add_succ(r, mp) : {bp == _ : Nat}
759	  h
760	
761	def internal_div_go_eq(n: Nat, m: Nat, +bp: Nat, +d: Nat, +r: Nat, +h: {bp == Nat.add(r, m) : Nat}) -> {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))) == Nat.add(n, Nat.add(Nat.mul(d, 1n+bp), r)) : Nat}:
762	  match n m:
763	    case 0n _:
764	      {==}
765	    case 1n++np 0n:
766	      %add_succ(np, Nat.add(Nat.mul(d, 1n+bp), r)) : {Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n))) == _ : Nat}
767	      %add_comm(r, Nat.mul(d, 1n+bp)) : {Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n))) == Nat.add(np, 1n+_) : Nat}
768	      %internal_div_block_start(bp, r, h) : {Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n))) == Nat.add(np, 1n+Nat.add(_, Nat.mul(d, 1n+bp))) : Nat}
769	      %add_zero(Nat.add(bp, Nat.mul(d, 1n+bp))) : {Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n))) == Nat.add(np, 1n+_) : Nat}
770	      internal_div_go_eq(np, r, bp, 1n+d, 0n, internal_div_block_start(bp, r, h))
771	    case 1n++np 1n++mp:
772	      %add_succ(np, Nat.add(Nat.mul(d, 1n+bp), r)) : {Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(np, mp, d, 1n+r)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(np, mp, d, 1n+r))) == _ : Nat}
773	      %add_succ(Nat.mul(d, 1n+bp), r) : {Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(np, mp, d, 1n+r)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(np, mp, d, 1n+r))) == Nat.add(np, _) : Nat}
774	      internal_div_go_eq(np, mp, bp, d, 1n+r, internal_div_block_step(bp, r, mp, h))
775	
776	# The division equation, for a positive divisor 1 + b: (a / (1 + b)) * (1 + b) + a % (1 + b) = a.
777	law div_mod_eq:
778	  for +a: Nat
779	  for +b: Nat
780	  {Nat.add(Nat.mul(Nat.div(a, 1n+b), 1n+b), Nat.mod(a, 1n+b)) == a : Nat}
781	
782	def div_mod_eq(a, b):
783	  %add_zero(a) : {Nat.add(Nat.mul(Nat.div(a, 1n+b), 1n+b), Nat.mod(a, 1n+b)) == _ : Nat}
784	  internal_div_go_eq(a, b, b, 0n, 0n, {==})
785	
786	def internal_div_wit_succ(+ap: Nat, +bq: Nat, w: &k:Nat -> {Nat.add(ap, k) == bq : Nat}) -> &k:Nat -> {Nat.add(1n+ap, k) == 1n+bq : Nat}:
787	  match w:
788	    case (k, e):
789	      (k, Equal.cong(Nat, Nat, x => 1n+x, Nat.add(ap, k), bq, e))
790	
791	def internal_div_le_wit(a: Nat, b: Nat, h: {Nat.is_le(a, b) == True{} : Bool}) -> &k:Nat -> {Nat.add(a, k) == b : Nat}:
792	  match a b:
793	    case 0n y:
794	      (y, {==})
795	    case 1n+ap 0n:
796	      Empty.absurd(&k:Nat -> {Nat.add(1n+ap, k) == 0n : Nat}, internal_false_ne_true(h))
797	    case 1n++ap 1n++bq:
798	      internal_div_wit_succ(ap, bq, internal_div_le_wit(ap, bq, h))
799	
800	def internal_div_go_small(n: Nat, +k: Nat, +d: Nat, r: Nat) -> {d == Pair.fst(Nat, Nat, Nat.divmod.go(n, Nat.add(n, k), d, r)) : Nat}:
801	  match n:
802	    case 0n:
803	      {==}
804	    case 1n+np:
805	      internal_div_go_small(np, k, d, 1n+r)
806	
807	def internal_div_zero_of_wit(+a: Nat, +b: Nat, w: &k:Nat -> {Nat.add(a, k) == b : Nat}) -> {Nat.div(a, 1n+b) == 0n : Nat}:
808	  match w:
809	    case (+k, e):
810	      %e : {Nat.div(a, 1n+_) == 0n : Nat}
811	      Equal.sym(Nat, 0n, Pair.fst(Nat, Nat, Nat.divmod.go(a, Nat.add(a, k), 0n, 0n)), internal_div_go_small(a, k, 0n, 0n))
812	
813	# A number at most b divides by 1 + b to zero: a <= b implies a / (1 + b) = 0.
814	law div_eq_zero_of_le:
815	  for +a: Nat
816	  for +b: Nat
817	  for h: le(a, b)
818	  {Nat.div(a, 1n+b) == 0n : Nat}
819	
820	def div_eq_zero_of_le(a, b, h):
821	  internal_div_zero_of_wit(a, b, internal_div_le_wit(a, b, h))
822	
823	def internal_div_le_succ_r(j: Nat, d: Nat, h: {True{} == Nat.is_le(j, d) : Bool}) -> {True{} == Nat.is_le(j, 1n+d) : Bool}:
824	  match j d:
825	    case 0n _:
826	      {==}
827	    case 1n+i 0n:
828	      Empty.absurd({True{} == Nat.is_le(1n+i, 1n) : Bool}, internal_div_true_ne_false(h))
829	    case 1n+i 1n+e:
830	      internal_div_le_succ_r(i, e, h)
831	
832	def internal_div_go_d_ge(+j: Nat, n: Nat, m: Nat, +d: Nat, r: Nat, h: {True{} == Nat.is_le(j, d) : Bool}) -> {True{} == Nat.is_le(j, Pair.fst(Nat, Nat, Nat.divmod.go(n, m, d, r))) : Bool}:
833	  match n m:
834	    case 0n _:
835	      h
836	    case 1n+np 0n:
837	      internal_div_go_d_ge(j, np, r, 1n+d, 0n, internal_div_le_succ_r(j, d, h))
838	    case 1n+np 1n+mp:
839	      internal_div_go_d_ge(j, np, mp, d, 1n+r, h)
840	
841	def internal_div_mono_go(a: Nat, m: Nat, +d: Nat, r: Nat, +k: Nat) -> {True{} == Nat.is_le(Pair.fst(Nat, Nat, Nat.divmod.go(a, m, d, r)), Pair.fst(Nat, Nat, Nat.divmod.go(Nat.add(a, k), m, d, r))) : Bool}:
842	  match a m:
843	    case 0n _:
844	      internal_div_go_d_ge(d, k, m, d, r, internal_div_le_refl(d))
845	    case 1n+ap 0n:
846	      internal_div_mono_go(ap, r, 1n+d, 0n, k)
847	    case 1n+ap 1n+mp:
848	      internal_div_mono_go(ap, mp, d, 1n+r, k)
849	
850	def internal_div_mono_wit(+a: Nat, +c: Nat, b: Nat, w: &k:Nat -> {Nat.add(a, k) == c : Nat}) -> le(Nat.div(a, 1n+b), Nat.div(c, 1n+b)):
851	  match w:
852	    case (+k, e):
853	      %e : le(Nat.div(a, 1n+b), Nat.div(_, 1n+b))
854	      Equal.sym(Bool, True{}, Nat.is_le(Nat.div(a, 1n+b), Nat.div(Nat.add(a, k), 1n+b)), internal_div_mono_go(a, b, 0n, 0n, k))
855	
856	# Division by a positive divisor is monotone: a <= c implies a / (1 + b) <= c / (1 + b).
857	law div_le_div:
858	  for +a: Nat
859	  for +c: Nat
860	  for b: Nat
861	  for h: le(a, c)
862	  le(Nat.div(a, 1n+b), Nat.div(c, 1n+b))
863	
864	def div_le_div(a, c, b, h):
865	  internal_div_mono_wit(a, c, b, internal_div_le_wit(a, c, h))
866	
867	def internal_div_go_shift(n: Nat, m: Nat, +d: Nat, +r: Nat) -> {1n+Pair.fst(Nat, Nat, Nat.divmod.go(n, m, d, r)) == Pair.fst(Nat, Nat, Nat.divmod.go(n, m, 1n+d, r)) : Nat}:
868	  match n m:
869	    case 0n _:
870	      {==}
871	    case 1n+np 0n:
872	      internal_div_go_shift(np, r, 1n+d, 0n)
873	    case 1n+np 1n+mp:
874	      internal_div_go_shift(np, mp, d, 1n+r)
875	
876	def internal_div_go_run(m: Nat, +a: Nat, +d: Nat, +r: Nat) -> {Nat.divmod.go(a, Nat.add(m, r), 1n+d, 0n) == Nat.divmod.go(Nat.add(1n+m, a), m, d, r) : Nat & Nat}:
877	  match m:
878	    case 0n:
879	      {==}
880	    case 1n++mp:
881	      %add_succ(mp, r) : {Nat.divmod.go(a, _, 1n+d, 0n) == Nat.divmod.go(1n+Nat.add(mp, a), mp, d, 1n+r) : Nat & Nat}
882	      internal_div_go_run(mp, a, d, 1n+r)
883	
884	# Adding the divisor adds one to the quotient: ((1 + b) + a) / (1 + b) = 1 + a / (1 + b).
885	law add_div_left:
886	  for +a: Nat
887	  for +b: Nat
888	  {Nat.div(Nat.add(1n+b, a), 1n+b) == 1n+Nat.div(a, 1n+b) : Nat}
889	
890	def add_div_left(a, b):
891	  %internal_div_go_run(b, a, 0n, 0n) : {Pair.fst(Nat, Nat, _) == 1n+Nat.div(a, 1n+b) : Nat}
892	  %internal_div_add_zero_r(b) : {Pair.fst(Nat, Nat, Nat.divmod.go(a, _, 1n, 0n)) == 1n+Nat.div(a, 1n+b) : Nat}
893	  Equal.sym(Nat, 1n+Nat.div(a, 1n+b), Pair.fst(Nat, Nat, Nat.divmod.go(a, b, 1n, 0n)), internal_div_go_shift(a, b, 0n, 0n))
894	
895	def internal_div_le_add_cancel(t: Nat, +x: Nat, +y: Nat) -> {Nat.is_le(x, y) == Nat.is_le(Nat.add(t, x), Nat.add(t, y)) : Bool}:
896	  match t:
897	    case 0n:
898	      {==}
899	    case 1n+tp:
900	      internal_div_le_add_cancel(tp, x, y)
901	
902	def internal_div_gt_add(a: Nat, +y: Nat) -> {False{} == Nat.is_le(1n+Nat.add(a, y), a) : Bool}:
903	  match a:
904	    case 0n:
905	      {==}
906	    case 1n+ap:
907	      internal_div_gt_add(ap, y)
908	
909	def internal_div_not_succ_le(a: Nat, bp: Nat, h: {False{} == Nat.is_le(1n+bp, a) : Bool}) -> {Nat.is_le(a, bp) == True{} : Bool}:
910	  match a bp:
911	    case 0n q:
912	      Equal.sym(Bool, True{}, Nat.is_le(0n, q), internal_div_zero_le(q))
913	    case 1n+ap 0n:
914	      Empty.absurd({Nat.is_le(1n+ap, 0n) == True{} : Bool}, internal_div_true_ne_false(Equal.sym(Bool, False{}, True{}, Equal.trans(Bool, False{}, Nat.is_le(0n, ap), True{}, h, Equal.sym(Bool, True{}, Nat.is_le(0n, ap), internal_div_zero_le(ap))))))
915	    case 1n+ap 1n+q:
916	      internal_div_not_succ_le(ap, q, h)
917	
918	def internal_div_le_big(+np: Nat, +a: Nat, +bp: Nat, w: &k:Nat -> {Nat.add(1n+bp, k) == a : Nat}, ih: @x:Nat -> {Nat.is_le(np, Nat.div(x, 1n+bp)) == Nat.is_le(Nat.mul(np, 1n+bp), x) : Bool}) -> {Nat.is_le(1n+np, Nat.div(a, 1n+bp)) == Nat.is_le(Nat.mul(1n+np, 1n+bp), a) : Bool}:
919	  match w:
920	    case (+k, e):
921	      %e : {Nat.is_le(1n+np, Nat.div(_, 1n+bp)) == Nat.is_le(1n+Nat.add(bp, Nat.mul(np, 1n+bp)), _) : Bool}
922	      %internal_div_le_add_cancel(bp, Nat.mul(np, 1n+bp), k) : {Nat.is_le(1n+np, Nat.div(1n+Nat.add(bp, k), 1n+bp)) == _ : Bool}
923	      %Equal.sym(Nat, Nat.div(Nat.add(1n+bp, k), 1n+bp), 1n+Nat.div(k, 1n+bp), add_div_left(k, bp)) : {Nat.is_le(1n+np, _) == Nat.is_le(Nat.mul(np, 1n+bp), k) : Bool}
924	      ih(k)
925	
926	def internal_div_le_small(+np: Nat, +a: Nat, +bp: Nat, w: &k:Nat -> {Nat.add(a, k) == bp : Nat}) -> {Nat.is_le(1n+np, Nat.div(a, 1n+bp)) == Nat.is_le(Nat.mul(1n+np, 1n+bp), a) : Bool}:
927	  match w:
928	    case (+k, e):
929	      %e : {Nat.is_le(1n+np, Nat.div(a, 1n+_)) == Nat.is_le(1n+Nat.add(_, Nat.mul(np, 1n+_)), a) : Bool}
930	      %internal_div_go_small(a, k, 0n, 0n) : {Nat.is_le(1n+np, _) == Nat.is_le(1n+Nat.add(Nat.add(a, k), Nat.mul(np, 1n+Nat.add(a, k))), a) : Bool}
931	      %Equal.sym(Nat, Nat.add(Nat.add(a, k), Nat.mul(np, 1n+Nat.add(a, k))), Nat.add(a, Nat.add(k, Nat.mul(np, 1n+Nat.add(a, k)))), add_assoc(a, k, Nat.mul(np, 1n+Nat.add(a, k)))) : {False{} == Nat.is_le(1n+_, a) : Bool}
932	      internal_div_gt_add(a, Nat.add(k, Nat.mul(np, 1n+Nat.add(a, k))))
933	
934	def internal_div_le_step(+np: Nat, +a: Nat, +bp: Nat, b: Bool, eb: {b == Nat.is_le(1n+bp, a) : Bool}, ih: @x:Nat -> {Nat.is_le(np, Nat.div(x, 1n+bp)) == Nat.is_le(Nat.mul(np, 1n+bp), x) : Bool}) -> {Nat.is_le(1n+np, Nat.div(a, 1n+bp)) == Nat.is_le(Nat.mul(1n+np, 1n+bp), a) : Bool}:
935	  match b:
936	    case True{}:
937	      internal_div_le_big(np, a, bp, internal_div_le_wit(1n+bp, a, Equal.sym(Bool, True{}, Nat.is_le(1n+bp, a), eb)), ih)
938	    case False{}:
939	      internal_div_le_small(np, a, bp, internal_div_le_wit(a, bp, internal_div_not_succ_le(a, bp, eb)))
940	
941	# A quotient is compared by multiplying back: n <= a / (1 + b) tests as n * (1 + b) <= a.
942	law le_div_iff_mul_le:
943	  for n: Nat
944	  for +a: Nat
945	  for +b: Nat
946	  {Nat.is_le(n, Nat.div(a, 1n+b)) == Nat.is_le(Nat.mul(n, 1n+b), a) : Bool}
947	
948	def le_div_iff_mul_le(n, a, b):
949	  match n:
950	    case 0n:
951	      %internal_div_zero_le(Nat.div(a, 1n+b)) : {_ == Nat.is_le(0n, a) : Bool}
952	      %internal_div_zero_le(a) : {True{} == _ : Bool}
953	      {==}
954	    case 1n++np:
955	      internal_div_le_step(np, a, b, Nat.is_le(1n+b, a), {==}, x => le_div_iff_mul_le(np, x, b))
956	
957	# Minimum is commutative.
958	law min_comm:
959	  for a: Nat
960	  for b: Nat
961	  {Nat.min(a, b) == Nat.min(b, a) : Nat}
962	
963	def min_comm(a, b):
964	  match a b:
965	    case 0n 0n:
966	      {==}
967	    case 0n 1n+q:
968	      {==}
969	    case 1n+p 0n:
970	      {==}
971	    case 1n++p 1n++q:
972	      %min_comm(p, q) : {1n+Nat.min(p, q) == 1n+_ : Nat}
973	      {==}
974	
975	# Maximum is commutative.
976	law max_comm:
977	  for a: Nat
978	  for b: Nat
979	  {Nat.max(a, b) == Nat.max(b, a) : Nat}
980	
981	def max_comm(a, b):
982	  match a b:
983	    case 0n 0n:
984	      {==}
985	    case 0n 1n+q:
986	      {==}
987	    case 1n+p 0n:
988	      {==}
989	    case 1n++p 1n++q:
990	      %max_comm(p, q) : {1n+Nat.max(p, q) == 1n+_ : Nat}
991	      {==}
992	
993	# The minimum of a natural and itself is itself.
994	law min_self:
995	  for a: Nat
996	  {Nat.min(a, a) == a : Nat}
997	
998	def min_self(a):
999	  match a:
1000	    case 0n:
1001	      {==}
1002	    case 1n++p:
1003	      %min_self(p) : {1n+Nat.min(p, p) == 1n+_ : Nat}
1004	      {==}
1005	
1006	# The maximum of a natural and itself is itself.
1007	law max_self:
1008	  for a: Nat
1009	  {Nat.max(a, a) == a : Nat}
1010	
1011	def max_self(a):
1012	  match a:
1013	    case 0n:
1014	      {==}
1015	    case 1n++p:
1016	      %max_self(p) : {1n+Nat.max(p, p) == 1n+_ : Nat}
1017	      {==}
1018	
1019	# The minimum with zero is zero: min(a, 0) = 0.
1020	law min_zero:
1021	  for a: Nat
1022	  {Nat.min(a, 0n) == 0n : Nat}
1023	
1024	def min_zero(a):
1025	  match a:
1026	    case 0n:
1027	      {==}
1028	    case 1n+p:
1029	      {==}
1030	
1031	# The minimum with zero is zero: min(0, a) = 0.
1032	law zero_min:
1033	  for a: Nat
1034	  {Nat.min(0n, a) == 0n : Nat}
1035	
1036	def zero_min(a):
1037	  match a:
1038	    case 0n:
1039	      {==}
1040	    case 1n+p:
1041	      {==}
1042	
1043	# Zero is an identity for maximum: max(a, 0) = a.
1044	law max_zero:
1045	  for a: Nat
1046	  {Nat.max(a, 0n) == a : Nat}
1047	
1048	def max_zero(a):
1049	  match a:
1050	    case 0n:
1051	      {==}
1052	    case 1n+p:
1053	      {==}
1054	
1055	# Zero is an identity for maximum: max(0, a) = a.
1056	law zero_max:
1057	  for a: Nat
1058	  {Nat.max(0n, a) == a : Nat}
1059	
1060	def zero_max(a):
1061	  match a:
1062	    case 0n:
1063	      {==}
1064	    case 1n+p:
1065	      {==}
1066	
1067	# Minimum is associative.
1068	law min_assoc:
1069	  for a: Nat
1070	  for b: Nat
1071	  for c: Nat
1072	  {Nat.min(Nat.min(a, b), c) == Nat.min(a, Nat.min(b, c)) : Nat}
1073	
1074	def min_assoc(a, b, c):
1075	  match a b c:
1076	    case 0n _ _:
1077	      {==}
1078	    case 1n+p 0n _:
1079	      {==}
1080	    case 1n+p 1n+q 0n:
1081	      {==}
1082	    case 1n++p 1n++q 1n++r:
1083	      %min_assoc(p, q, r) : {1n+Nat.min(Nat.min(p, q), r) == 1n+_ : Nat}
1084	      {==}
1085	
1086	# Maximum is associative.
1087	law max_assoc:
1088	  for a: Nat
1089	  for b: Nat
1090	  for c: Nat
1091	  {Nat.max(Nat.max(a, b), c) == Nat.max(a, Nat.max(b, c)) : Nat}
1092	
1093	def max_assoc(a, b, c):
1094	  match a b c:
1095	    case 0n _ _:
1096	      {==}
1097	    case 1n+p 0n _:
1098	      {==}
1099	    case 1n+p 1n+q 0n:
1100	      {==}
1101	    case 1n++p 1n++q 1n++r:
1102	      %max_assoc(p, q, r) : {1n+Nat.max(Nat.max(p, q), r) == 1n+_ : Nat}
1103	      {==}
1104	
1105	# The minimum plus the maximum is the sum: min(a, b) + max(a, b) = a + b.
1106	law min_add_max:
1107	  for a: Nat
1108	  for b: Nat
1109	  {Nat.add(Nat.min(a, b), Nat.max(a, b)) == Nat.add(a, b) : Nat}
1110	
1111	def min_add_max(a, b):
1112	  match a b:
1113	    case 0n 0n:
1114	      {==}
1115	    case 0n 1n+q:
1116	      {==}
1117	    case 1n++p 0n:
1118	      %add_zero(p) : {1n+_ == 1n+Nat.add(p, 0n) : Nat}
1119	      {==}
1120	    case 1n++p 1n++q:
1121	      %Equal.sym(Nat, Nat.add(Nat.min(p, q), 1n+Nat.max(p, q)), 1n+Nat.add(Nat.min(p, q), Nat.max(p, q)), add_succ(Nat.min(p, q), Nat.max(p, q))) : {1n+_ == 1n+Nat.add(p, 1n+q) : Nat}
1122	      %Equal.sym(Nat, Nat.add(p, 1n+q), 1n+Nat.add(p, q), add_succ(p, q)) : {2n+Nat.add(Nat.min(p, q), Nat.max(p, q)) == 1n+_ : Nat}
1123	      %min_add_max(p, q) : {2n+Nat.add(Nat.min(p, q), Nat.max(p, q)) == 2n+_ : Nat}
1124	      {==}
1125	
1126	# The minimum is at most its left argument.
1127	law min_le_left:
1128	  for a: Nat
1129	  for b: Nat
1130	  le(Nat.min(a, b), a)
1131	
1132	def min_le_left(a, b):
1133	  match a b:
1134	    case 0n 0n:
1135	      {==}
1136	    case 0n 1n+q:
1137	      {==}
1138	    case 1n+p 0n:
1139	      {==}
1140	    case 1n+p 1n+q:
1141	      min_le_left(p, q)
1142	
1143	# The minimum is at most its right argument.
1144	law min_le_right:
1145	  for a: Nat
1146	  for b: Nat
1147	  le(Nat.min(a, b), b)
1148	
1149	def min_le_right(a, b):
1150	  match a b:
1151	    case 0n 0n:
1152	      {==}
1153	    case 0n 1n+q:
1154	      {==}
1155	    case 1n+p 0n:
1156	      {==}
1157	    case 1n+p 1n+q:
1158	      min_le_right(p, q)
1159	
1160	# The left argument is at most the maximum.
1161	law le_max_left:
1162	  for a: Nat
1163	  for b: Nat
1164	  le(a, Nat.max(a, b))
1165	
1166	def le_max_left(a, b):
1167	  match a b:
1168	    case 0n 0n:
1169	      {==}
1170	    case 0n 1n+q:
1171	      {==}
1172	    case 1n+p 0n:
1173	      le_refl(1n+p)
1174	    case 1n+p 1n+q:
1175	      le_max_left(p, q)
1176	
1177	# The right argument is at most the maximum.
1178	law le_max_right:
1179	  for a: Nat
1180	  for b: Nat
1181	  le(b, Nat.max(a, b))
1182	
1183	def le_max_right(a, b):
1184	  match a b:
1185	    case 0n 0n:
1186	      {==}
1187	    case 0n 1n+q:
1188	      le_refl(1n+q)
1189	    case 1n+p 0n:
1190	      {==}
1191	    case 1n+p 1n+q:
1192	      le_max_right(p, q)
1193	
1194	# Any natural to the power zero is one.
1195	law pow_zero:
1196	  for -a: Nat
1197	  {Nat.pow(a, 0n) == 1n : Nat}
1198	
1199	def pow_zero(a):
1200	  {==}
1201	
1202	# A power with a successor exponent: a^(n+1) = a * a^n.
1203	law pow_succ:
1204	  for -a: Nat
1205	  for -n: Nat
1206	  {Nat.pow(a, 1n+n) == Nat.mul(a, Nat.pow(a, n)) : Nat}
1207	
1208	def pow_succ(a, n):
1209	  {==}
1210	
1211	# Any natural to the power one is itself.
1212	law pow_one:
1213	  for a: Nat
1214	  {Nat.pow(a, 1n) == a : Nat}
1215	
1216	def pow_one(a):
1217	  mul_one(a)
1218	
1219	# One to any power is one.
1220	law one_pow:
1221	  for n: Nat
1222	  {Nat.pow(1n, n) == 1n : Nat}
1223	
1224	def one_pow(n):
1225	  match n:
1226	    case 0n:
1227	      {==}
1228	    case 1n++p:
1229	      %Equal.sym(Nat, Nat.mul(1n, Nat.pow(1n, p)), Nat.pow(1n, p), one_mul(Nat.pow(1n, p))) : {_ == 1n : Nat}
1230	      one_pow(p)
1231	
1232	# Exponents add under multiplication: a^(m+n) = a^m * a^n.
1233	law pow_add:
1234	  for a: Nat
1235	  for m: Nat
1236	  for n: Nat
1237	  {Nat.pow(a, Nat.add(m, n)) == Nat.mul(Nat.pow(a, m), Nat.pow(a, n)) : Nat}
1238	
1239	def pow_add(a, m, n):
1240	  match m:
1241	    case 0n:
1242	      +a = a
1243	      +n = n
1244	      %Equal.sym(Nat, Nat.mul(1n, Nat.pow(a, n)), Nat.pow(a, n), one_mul(Nat.pow(a, n))) : {Nat.pow(a, n) == _ : Nat}
1245	      {==}
1246	    case 1n++p:
1247	      +a = a
1248	      +n = n
1249	      %Equal.sym(Nat, Nat.pow(a, Nat.add(p, n)), Nat.mul(Nat.pow(a, p), Nat.pow(a, n)), pow_add(a, p, n)) : {Nat.mul(a, _) == Nat.mul(Nat.mul(a, Nat.pow(a, p)), Nat.pow(a, n)) : Nat}
1250	      Equal.sym(Nat, Nat.mul(Nat.mul(a, Nat.pow(a, p)), Nat.pow(a, n)), Nat.mul(a, Nat.mul(Nat.pow(a, p), Nat.pow(a, n))), mul_assoc(a, Nat.pow(a, p), Nat.pow(a, n)))
1251	
1252	# Doubling is adding a natural to itself.
1253	law double_eq_add:
1254	  for n: Nat
1255	  {Nat.double(n) == Nat.add(n, n) : Nat}
1256	
1257	def double_eq_add(n):
1258	  match n:
1259	    case 0n:
1260	      {==}
1261	    case 1n++p:
1262	      %Equal.sym(Nat, Nat.add(p, 1n+p), 1n+Nat.add(p, p), add_succ(p, p)) : {2n+Nat.double(p) == 1n+_ : Nat}
1263	      %double_eq_add(p) : {2n+Nat.double(p) == 2n+_ : Nat}
1264	      {==}
1265	
1266	# Every natural tests equal to itself.
1267	law is_eq_refl:
1268	  for n: Nat
1269	  {Nat.is_eq(n, n) == True{} : Bool}
1270	
1271	def is_eq_refl(n):
1272	  match n:
1273	    case 0n:
1274	      {==}
1275	    case 1n+p:
1276	      is_eq_refl(p)
1277	
1278	# The equality test is symmetric.
1279	law is_eq_comm:
1280	  for a: Nat
1281	  for b: Nat
1282	  {Nat.is_eq(a, b) == Nat.is_eq(b, a) : Bool}
1283	
1284	def is_eq_comm(a, b):
1285	  match a b:
1286	    case 0n 0n:
1287	      {==}
1288	    case 0n 1n+q:
1289	      {==}
1290	    case 1n+p 0n:
1291	      {==}
1292	    case 1n++p 1n++q:
1293	      %is_eq_comm(p, q) : {Nat.is_eq(p, q) == _ : Bool}
1294	      {==}
1295	
1296	# If the equality test says true, the naturals are equal.
1297	law eq_of_is_eq:
1298	  for a: Nat
1299	  for b: Nat
1300	  for h: {Nat.is_eq(a, b) == True{} : Bool}
1301	  {a == b : Nat}
1302	
1303	def eq_of_is_eq(a, b, h):
1304	  match a b:
1305	    case 0n 0n:
1306	      {==}
1307	    case 0n 1n+q:
1308	      Empty.absurd({0n == 1n+q : Nat}, internal_false_ne_true(h))
1309	    case 1n+p 0n:
1310	      Empty.absurd({1n+p == 0n : Nat}, internal_false_ne_true(h))
1311	    case 1n++p 1n++q:
1312	      %eq_of_is_eq(p, q, h) : {1n+p == 1n+_ : Nat}
1313	      {==}
1314	
1315	# A >= b tests the same as b <= a.
1316	law is_ge_eq_is_le:
1317	  for a: Nat
1318	  for b: Nat
1319	  {Nat.is_ge(a, b) == Nat.is_le(b, a) : Bool}
1320	
1321	def is_ge_eq_is_le(a, b):
1322	  match a b:
1323	    case 0n 0n:
1324	      {==}
1325	    case 0n 1n+q:
1326	      {==}
1327	    case 1n+p 0n:
1328	      {==}
1329	    case 1n++p 1n++q:
1330	      %is_ge_eq_is_le(p, q) : {Nat.is_ge(p, q) == _ : Bool}
1331	      {==}
1332	
1333	# A > b tests the same as b < a.
1334	law is_gt_eq_is_lt:
1335	  for a: Nat
1336	  for b: Nat
1337	  {Nat.is_gt(a, b) == Nat.is_lt(b, a) : Bool}
1338	
1339	def is_gt_eq_is_lt(a, b):
1340	  match a b:
1341	    case 0n 0n:
1342	      {==}
1343	    case 0n 1n+q:
1344	      {==}
1345	    case 1n+p 0n:
1346	      {==}
1347	    case 1n++p 1n++q:
1348	      %is_gt_eq_is_lt(p, q) : {Nat.is_gt(p, q) == _ : Bool}
1349	      {==}
1350	
1351	# A < b tests the same as a + 1 <= b.
1352	law is_lt_eq_succ_le:
1353	  for a: Nat
1354	  for b: Nat
1355	  {Nat.is_lt(a, b) == Nat.is_le(1n+a, b) : Bool}
1356	
1357	def is_lt_eq_succ_le(a, b):
1358	  match a b:
1359	    case 0n 0n:
1360	      {==}
1361	    case 0n 1n+q:
1362	      match q:
1363	        case 0n:
1364	          {==}
1365	        case 1n+r:
1366	          {==}
1367	    case 1n+p 0n:
1368	      {==}
1369	    case 1n+p 1n+q:
1370	      is_lt_eq_succ_le(p, q)
1371	
1372	# Not (a <= b) tests the same as b < a.
1373	law not_is_le:
1374	  for a: Nat
1375	  for b: Nat
1376	  {Bool.not(Nat.is_le(a, b)) == Nat.is_lt(b, a) : Bool}
1377	
1378	def not_is_le(a, b):
1379	  match a b:
1380	    case 0n 0n:
1381	      {==}
1382	    case 0n 1n+q:
1383	      {==}
1384	    case 1n+p 0n:
1385	      {==}
1386	    case 1n+p 1n+q:
1387	      not_is_le(p, q)
1388	
1389	# Not (a < b) tests the same as b <= a.
1390	law not_is_lt:
1391	  for a: Nat
1392	  for b: Nat
1393	  {Bool.not(Nat.is_lt(a, b)) == Nat.is_le(b, a) : Bool}
1394	
1395	def not_is_lt(a, b):
1396	  match a b:
1397	    case 0n 0n:
1398	      {==}
1399	    case 0n 1n+q:
1400	      {==}
1401	    case 1n+p 0n:
1402	      {==}
1403	    case 1n+p 1n+q:
1404	      not_is_lt(p, q)
1405	
1406	# Every natural is less than its successor: n < n + 1.
1407	law lt_succ_self:
1408	  for n: Nat
1409	  lt(n, 1n+n)
1410	
1411	def lt_succ_self(n):
1412	  match n:
1413	    case 0n:
1414	      {==}
1415	    case 1n+p:
1416	      lt_succ_self(p)
1417	
1418	# The successor preserves the order: a <= b implies a + 1 <= b + 1.
1419	law succ_le_succ:
1420	  for -a: Nat
1421	  for -b: Nat
1422	  for h: le(a, b)
1423	  le(1n+a, 1n+b)
1424	
1425	def succ_le_succ(a, b, h):
1426	  h
1427	
1428	# The order of successors is the order of the naturals: a + 1 <= b + 1 implies a <= b.
1429	law le_of_succ_le_succ:
1430	  for -a: Nat
1431	  for -b: Nat
1432	  for h: le(1n+a, 1n+b)
1433	  le(a, b)
1434	
1435	def le_of_succ_le_succ(a, b, h):
1436	  h
1437	
1438	# A < b and b <= c imply a < c.
1439	law lt_of_lt_of_le:
1440	  for a: Nat
1441	  for b: Nat
1442	  for c: Nat
1443	  for ab: lt(a, b)
1444	  for bc: le(b, c)
1445	  lt(a, c)
1446	
1447	def lt_of_lt_of_le(a, b, c, ab, bc):
1448	  match a b c:
1449	    case 0n 0n _:
1450	      Empty.absurd(lt(0n, c), internal_false_ne_true(ab))
1451	    case 0n 1n+q 0n:
1452	      Empty.absurd(lt(0n, 0n), internal_false_ne_true(bc))
1453	    case 0n 1n+q 1n+r:
1454	      {==}
1455	    case 1n+p 0n _:
1456	      Empty.absurd(lt(1n+p, c), internal_false_ne_true(ab))
1457	    case 1n+p 1n+q 0n:
1458	      Empty.absurd(lt(1n+p, 0n), internal_false_ne_true(bc))
1459	    case 1n+p 1n+q 1n+r:
1460	      lt_of_lt_of_le(p, q, r, ab, bc)
1461	
1462	# A <= b and b < c imply a < c.
1463	law lt_of_le_of_lt:
1464	  for a: Nat
1465	  for b: Nat
1466	  for c: Nat
1467	  for ab: le(a, b)
1468	  for bc: lt(b, c)
1469	  lt(a, c)
1470	
1471	def lt_of_le_of_lt(a, b, c, ab, bc):
1472	  match a b c:
1473	    case 0n 0n 0n:
1474	      Empty.absurd(lt(0n, 0n), internal_false_ne_true(bc))
1475	    case 0n 1n+q 0n:
1476	      Empty.absurd(lt(0n, 0n), internal_false_ne_true(bc))
1477	    case 0n _ 1n+r:
1478	      {==}
1479	    case 1n+p 0n _:
1480	      Empty.absurd(lt(1n+p, c), internal_false_ne_true(ab))
1481	    case 1n+p 1n+q 0n:
1482	      Empty.absurd(lt(1n+p, 0n), internal_false_ne_true(bc))
1483	    case 1n+p 1n+q 1n+r:
1484	      lt_of_le_of_lt(p, q, r, ab, bc)
1485	
1486	# Adding on the left preserves the order: a <= b implies k + a <= k + b.
1487	law add_le_add_left:
1488	  for -a: Nat
1489	  for -b: Nat
1490	  for k: Nat
1491	  for h: le(a, b)
1492	  le(Nat.add(k, a), Nat.add(k, b))
1493	
1494	def add_le_add_left(a, b, k, h):
1495	  match k:
1496	    case 0n:
1497	      h
1498	    case 1n+p:
1499	      add_le_add_left(a, b, p, h)
1500	
1501	# Adding on the right preserves the order: a <= b implies a + k <= b + k.
1502	law add_le_add_right:
1503	  for +a: Nat
1504	  for +b: Nat
1505	  for +k: Nat
1506	  for h: le(a, b)
1507	  le(Nat.add(a, k), Nat.add(b, k))
1508	
1509	def add_le_add_right(a, b, k, h):
1510	  %add_comm(k, a) : le(_, Nat.add(b, k))
1511	  %add_comm(k, b) : le(Nat.add(k, a), _)
1512	  add_le_add_left(a, b, k, h)
1513	
1514	# Adding the same amount on the left does not change the order test: a <= b tests as k + a <= k + b.
1515	law add_le_add_iff_left:
1516	  for k: Nat
1517	  for -a: Nat
1518	  for -b: Nat
1519	  {Nat.is_le(a, b) == Nat.is_le(Nat.add(k, a), Nat.add(k, b)) : Bool}
1520	
1521	def add_le_add_iff_left(k, a, b):
1522	  match k:
1523	    case 0n:
1524	      {==}
1525	    case 1n+p:
1526	      add_le_add_iff_left(p, a, b)
1527	
1528	# Adding two bounded summands stays bounded: a <= c and b <= d imply a + b <= c + d.
1529	law add_le_add:
1530	  for +a: Nat
1531	  for +b: Nat
1532	  for +c: Nat
1533	  for +d: Nat
1534	  for h1: le(a, c)
1535	  for h2: le(b, d)
1536	  le(Nat.add(a, b), Nat.add(c, d))
1537	
1538	def add_le_add(a, b, c, d, h1, h2):
1539	  le_trans(Nat.add(a, b), Nat.add(c, b), Nat.add(c, d), add_le_add_right(a, c, b, h1), add_le_add_left(b, d, c, h2))
1540	
1541	# A sum is at most c exactly when a <= c and b <= c - a: a + b <= c tests as both.
1542	law le_and_le_sub_iff_add_le:
1543	  for a: Nat
1544	  for -b: Nat
1545	  for c: Nat
1546	  {Bool.and(Nat.is_le(a, c), Nat.is_le(b, Nat.sub(c, a))) == Nat.is_le(Nat.add(a, b), c) : Bool}
1547	
1548	def le_and_le_sub_iff_add_le(a, b, c):
1549	  match a c:
1550	    case 0n 0n:
1551	      {==}
1552	    case 0n 1n+j:
1553	      {==}
1554	    case 1n+i 0n:
1555	      {==}
1556	    case 1n+i 1n+j:
1557	      le_and_le_sub_iff_add_le(i, b, j)
1558	
1559	# The only natural at most zero is zero.
1560	law le_zero_eq:
1561	  for n: Nat
1562	  for h: le(n, 0n)
1563	  {n == 0n : Nat}
1564	
1565	def le_zero_eq(n, h):
1566	  match n:
1567	    case 0n:
1568	      {==}
1569	    case 1n+p:
1570	      Empty.absurd({1n+p == 0n : Nat}, internal_false_ne_true(h))
1571	
1572	# No natural is less than zero.
1573	law lt_zero:
1574	  for n: Nat
1575	  lt(n, 0n) -> Empty
1576	
1577	def lt_zero(n):
1578	  match n:
1579	    case 0n:
1580	      h => internal_false_ne_true(h)
1581	    case 1n+p:
1582	      h => internal_false_ne_true(h)
1583	
1584	# A strict inequality rules out the reverse weak one: a < b implies b <= a is false.
1585	law not_le_of_lt:
1586	  for a: Nat
1587	  for b: Nat
1588	  for h: lt(a, b)
1589	  {Nat.is_le(b, a) == False{} : Bool}
1590	
1591	def not_le_of_lt(a, b, h):
1592	  match a b:
1593	    case 0n 0n:
1594	      Empty.absurd({Nat.is_le(0n, 0n) == False{} : Bool}, internal_false_ne_true(h))
1595	    case 0n 1n+q:
1596	      {==}
1597	    case 1n+p 0n:
1598	      Empty.absurd({Nat.is_le(0n, 1n+p) == False{} : Bool}, internal_false_ne_true(h))
1599	    case 1n+p 1n+q:
1600	      not_le_of_lt(p, q, h)
1601	
1602	# A weak inequality rules out the reverse strict one: a <= b implies b < a is false.
1603	law not_lt_of_le:
1604	  for a: Nat
1605	  for b: Nat
1606	  for h: le(a, b)
1607	  {Nat.is_lt(b, a) == False{} : Bool}
1608	
1609	def not_lt_of_le(a, b, h):
1610	  match a b:
1611	    case 0n 0n:
1612	      {==}
1613	    case 0n 1n+q:
1614	      {==}
1615	    case 1n+p 0n:
1616	      Empty.absurd({Nat.is_lt(0n, 1n+p) == False{} : Bool}, internal_false_ne_true(h))
1617	    case 1n+p 1n+q:
1618	      not_lt_of_le(p, q, h)
1619	
1620	# A failed weak test gives the reverse strict order: a <= b false implies b < a.
1621	law lt_of_not_le:
1622	  for a: Nat
1623	  for b: Nat
1624	  for h: {Nat.is_le(a, b) == False{} : Bool}
1625	  lt(b, a)
1626	
1627	def lt_of_not_le(a, b, h):
1628	  match a b:
1629	    case 0n 0n:
1630	      Empty.absurd(lt(0n, 0n), internal_false_ne_true(Equal.sym(Bool, True{}, False{}, h)))
1631	    case 0n 1n+q:
1632	      Empty.absurd(lt(1n+q, 0n), internal_false_ne_true(Equal.sym(Bool, True{}, False{}, h)))
1633	    case 1n+p 0n:
1634	      {==}
1635	    case 1n+p 1n+q:
1636	      lt_of_not_le(p, q, h)
1637	
1638	# A failed strict test gives the reverse weak order: a < b false implies b <= a.
1639	law le_of_not_lt:
1640	  for a: Nat
1641	  for b: Nat
1642	  for h: {Nat.is_lt(a, b) == False{} : Bool}
1643	  le(b, a)
1644	
1645	def le_of_not_lt(a, b, h):
1646	  match a b:
1647	    case 0n 0n:
1648	      {==}
1649	    case 0n 1n+q:
1650	      Empty.absurd(le(1n+q, 0n), internal_false_ne_true(Equal.sym(Bool, True{}, False{}, h)))
1651	    case 1n+p 0n:
1652	      {==}
1653	    case 1n+p 1n+q:
1654	      le_of_not_lt(p, q, h)
1655	
1656	# A number below both bounds is below their minimum: a < b and a < c imply a < min b c.
1657	law lt_min:
1658	  for a: Nat
1659	  for b: Nat
1660	  for c: Nat
1661	  for hb: lt(a, b)
1662	  for hc: lt(a, c)
1663	  lt(a, Nat.min(b, c))
1664	
1665	def lt_min(a, b, c, hb, hc):
1666	  match a b c:
1667	    case _ 0n _:
1668	      Empty.absurd(lt(a, Nat.min(0n, c)), lt_zero(a)(hb))
1669	    case _ 1n+q 0n:
1670	      Empty.absurd(lt(a, Nat.min(1n+q, 0n)), lt_zero(a)(hc))
1671	    case 0n 1n+q 1n+r:
1672	      {==}
1673	    case 1n+p 1n+q 1n+r:
1674	      lt_min(p, q, r, hb, hc)
1675	
1676	def internal_or_true_sym(x: Bool) -> {True{} == Bool.or(x, True{}) : Bool}:
1677	  match x:
1678	    case False{}:
1679	      {==}
1680	    case True{}:
1681	      {==}
1682	
1683	def internal_or_false_sym(x: Bool) -> {x == Bool.or(x, False{}) : Bool}:
1684	  match x:
1685	    case False{}:
1686	      {==}
1687	    case True{}:
1688	      {==}
1689	
1690	# The minimum is at most c exactly when one argument is: min a b <= c tests as a <= c or b <= c.
1691	law min_le_iff:
1692	  for a: Nat
1693	  for b: Nat
1694	  for c: Nat
1695	  {Nat.is_le(Nat.min(a, b), c) == Bool.or(Nat.is_le(a, c), Nat.is_le(b, c)) : Bool}
1696	
1697	def min_le_iff(a, b, c):
1698	  match a b c:
1699	    case 0n 0n 0n:
1700	      {==}
1701	    case 0n 0n 1n+r:
1702	      {==}
1703	    case 0n 1n+q 0n:
1704	      {==}
1705	    case 0n 1n+q 1n+r:
1706	      {==}
1707	    case 1n+p 0n 0n:
1708	      {==}
1709	    case 1n+p 0n 1n+r:
1710	      internal_or_true_sym(Nat.is_le(p, r))
1711	    case 1n+p 1n+q 0n:
1712	      {==}
1713	    case 1n+p 1n+q 1n+r:
1714	      min_le_iff(p, q, r)
1715	
1716	# The maximum is above a exactly when one argument is: a < max b c tests as a < b or a < c.
1717	law lt_max_iff:
1718	  for a: Nat
1719	  for b: Nat
1720	  for c: Nat
1721	  {Nat.is_lt(a, Nat.max(b, c)) == Bool.or(Nat.is_lt(a, b), Nat.is_lt(a, c)) : Bool}
1722	
1723	def lt_max_iff(a, b, c):
1724	  match a b c:
1725	    case 0n 0n 0n:
1726	      {==}
1727	    case 0n 0n 1n+r:
1728	      {==}
1729	    case 0n 1n+q 0n:
1730	      {==}
1731	    case 0n 1n+q 1n+r:
1732	      {==}
1733	    case 1n+p 0n 0n:
1734	      {==}
1735	    case 1n+p 0n 1n+r:
1736	      {==}
1737	    case 1n+p 1n+q 0n:
1738	      internal_or_false_sym(Nat.is_lt(p, q))
1739	    case 1n+p 1n+q 1n+r:
1740	      lt_max_iff(p, q, r)
1741	
1742	# Subtracting a larger number gives zero: a <= b implies a - b = 0.
1743	law sub_eq_zero_of_le:
1744	  for a: Nat
1745	  for b: Nat
1746	  for h: le(a, b)
1747	  {Nat.sub(a, b) == 0n : Nat}
1748	
1749	def sub_eq_zero_of_le(a, b, h):
1750	  match a b:
1751	    case 0n 0n:
1752	      {==}
1753	    case 0n 1n+q:
1754	      {==}
1755	    case 1n+p 0n:
1756	      Empty.absurd({Nat.sub(1n+p, 0n) == 0n : Nat}, internal_false_ne_true(h))
1757	    case 1n+p 1n+q:
1758	      sub_eq_zero_of_le(p, q, h)
1759	
1760	# Above the subtrahend, a successor subtracts to a successor: b <= a implies (a + 1) - b = (a - b) + 1.
1761	law succ_sub:
1762	  for a: Nat
1763	  for b: Nat
1764	  for h: le(b, a)
1765	  {Nat.sub(1n+a, b) == 1n+Nat.sub(a, b) : Nat}
1766	
1767	def succ_sub(a, b, h):
1768	  match a b:
1769	    case 0n 0n:
1770	      {==}
1771	    case 1n+p 0n:
1772	      {==}
1773	    case 0n 1n+q:
1774	      Empty.absurd({Nat.sub(1n, 1n+q) == 1n+Nat.sub(0n, 1n+q) : Nat}, internal_false_ne_true(h))
1775	    case 1n+p 1n+q:
1776	      succ_sub(p, q, h)
1777	
1778	# Adding back what was subtracted restores the number: a <= b implies a + (b - a) = b.
1779	law add_sub_of_le:
1780	  for a: Nat
1781	  for b: Nat
1782	  for h: le(a, b)
1783	  {Nat.add(a, Nat.sub(b, a)) == b : Nat}
1784	
1785	def add_sub_of_le(a, b, h):
1786	  match a b:
1787	    case 0n 0n:
1788	      {==}
1789	    case 0n 1n+q:
1790	      {==}
1791	    case 1n+p 0n:
1792	      Empty.absurd({Nat.add(1n+p, Nat.sub(0n, 1n+p)) == 0n : Nat}, internal_false_ne_true(h))
1793	    case 1n++p 1n++q:
1794	      %Equal.sym(Nat, Nat.add(p, Nat.sub(q, p)), q, add_sub_of_le(p, q, h)) : {1n+_ == 1n+q : Nat}
1795	      {==}
1796	
1797	def internal_lt_sub_zero(a: Nat, p: Nat) -> {Nat.is_lt(a, Nat.sub(0n, 1n+p)) == Nat.is_lt(Nat.add(1n+p, a), 0n) : Bool}:
1798	  match a:
1799	    case 0n:
1800	      {==}
1801	    case 1n+x:
1802	      {==}
1803	
1804	# Comparing against a difference is comparing the sum: a < c - b tests as b + a < c.
1805	law lt_sub_iff_add_lt:
1806	  for a: Nat
1807	  for b: Nat
1808	  for c: Nat
1809	  {Nat.is_lt(a, Nat.sub(c, b)) == Nat.is_lt(Nat.add(b, a), c) : Bool}
1810	
1811	def lt_sub_iff_add_lt(a, b, c):
1812	  match b c:
1813	    case 0n 0n:
1814	      {==}
1815	    case 0n 1n+r:
1816	      {==}
1817	    case 1n+p 0n:
1818	      internal_lt_sub_zero(a, p)
1819	    case 1n+p 1n+r:
1820	      lt_sub_iff_add_lt(a, p, r)
1821	
1822	# A witnessed difference gives the order: a + k = b implies a <= b.
1823	law le_of_add_eq:
1824	  for a: Nat
1825	  for k: Nat
1826	  for -b: Nat
1827	  for e: {Nat.add(a, k) == b : Nat}
1828	  le(a, b)
1829	
1830	def le_of_add_eq(a, k, b, e):
1831	  %e : {Nat.is_le(a, _) == True{} : Bool}
1832	  le_add_right(a, k)
1833	
1834	# Multiplying on the right preserves the order: a <= b implies a * k <= b * k.
1835	law mul_le_mul_right:
1836	  for +a: Nat
1837	  for +b: Nat
1838	  for +k: Nat
1839	  for h: le(a, b)
1840	  le(Nat.mul(a, k), Nat.mul(b, k))
1841	
1842	def mul_le_mul_right(a, b, k, h):
1843	  %sub_add_cancel(b, a, h) : {Nat.is_le(Nat.mul(a, k), Nat.mul(_, k)) == True{} : Bool}
1844	  %Equal.sym(Nat, Nat.mul(Nat.add(Nat.sub(b, a), a), k), Nat.add(Nat.mul(Nat.sub(b, a), k), Nat.mul(a, k)), add_mul(Nat.sub(b, a), a, k)) : {Nat.is_le(Nat.mul(a, k), _) == True{} : Bool}
1845	  %add_comm(Nat.mul(a, k), Nat.mul(Nat.sub(b, a), k)) : {Nat.is_le(Nat.mul(a, k), _) == True{} : Bool}
1846	  le_add_right(Nat.mul(a, k), Nat.mul(Nat.sub(b, a), k))
1847	
1848	# Zero divided by anything is zero: 0 / b = 0.
1849	law zero_div:
1850	  for b: Nat
1851	  {Nat.div(0n, b) == 0n : Nat}
1852	
1853	def zero_div(b):
1854	  match b:
1855	    case 0n:
1856	      {==}
1857	    case 1n+p:
1858	      {==}
1859	
1860	# Zero modulo anything is zero: 0 % b = 0.
1861	law zero_mod:
1862	  for b: Nat
1863	  {Nat.mod(0n, b) == 0n : Nat}
1864	
1865	def zero_mod(b):
1866	  match b:
1867	    case 0n:
1868	      {==}
1869	    case 1n+p:
1870	      {==}
1871	
1872	def internal_div_go_one(a: Nat, +d: Nat) -> {(Nat.add(a, d), 0n) == Nat.divmod.go(a, 0n, d, 0n) : Nat & Nat}:
1873	  match a:
1874	    case 0n:
1875	      {==}
1876	    case 1n++p:
1877	      %add_succ(p, d) : {(_, 0n) == Nat.divmod.go(p, 0n, 1n+d, 0n) : Nat & Nat}
1878	      internal_div_go_one(p, 1n+d)
1879	
1880	# Dividing by one changes nothing: a / 1 = a.
1881	law div_one:
1882	  for a: Nat
1883	  {Nat.div(a, 1n) == a : Nat}
1884	
1885	def div_one(a):
1886	  +a = a
1887	  %internal_div_go_one(a, 0n) : {Pair.fst(Nat, Nat, _) == a : Nat}
1888	  add_zero(a)
1889	
1890	# Any natural modulo one is zero: a % 1 = 0.
1891	law mod_one:
1892	  for a: Nat
1893	  {Nat.mod(a, 1n) == 0n : Nat}
1894	
1895	def mod_one(a):
1896	  +a = a
1897	  %internal_div_go_one(a, 0n) : {Pair.snd(Nat, Nat, _) == 0n : Nat}
1898	  {==}
1899	
1900	def internal_div_go_self(m: Nat, -d: Nat, -r: Nat) -> {(1n+d, 0n) == Nat.divmod.go(1n+m, m, d, r) : Nat & Nat}:
1901	  match m:
1902	    case 0n:
1903	      {==}
1904	    case 1n+p:
1905	      internal_div_go_self(p, d, 1n+r)
1906	
1907	# A natural modulo itself is zero: n % n = 0.
1908	law mod_self:
1909	  for n: Nat
1910	  {Nat.mod(n, n) == 0n : Nat}
1911	
1912	def mod_self(n):
1913	  match n:
1914	    case 0n:
1915	      {==}
1916	    case 1n++p:
1917	      %internal_div_go_self(p, 0n, 0n) : {Pair.snd(Nat, Nat, _) == 0n : Nat}
1918	      {==}
1919	
1920	# A positive natural divided by itself is one: (1 + b) / (1 + b) = 1.
1921	law div_self:
1922	  for b: Nat
1923	  {Nat.div(1n+b, 1n+b) == 1n : Nat}
1924	
1925	def div_self(b):
1926	  +b = b
1927	  %internal_div_go_self(b, 0n, 0n) : {Pair.fst(Nat, Nat, _) == 1n : Nat}
1928	  {==}
1929	
1930	def internal_mod_go_le(n: Nat, m: Nat, -d: Nat, +r: Nat) -> le(Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d, r)), Nat.add(r, m)):
1931	  match n m:
1932	    case 0n k:
1933	      le_add_right(r, k)
1934	    case 1n++np 0n:
1935	      %internal_div_add_zero_r(r) : le(Pair.snd(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n)), _)
1936	      internal_mod_go_le(np, r, 1n+d, 0n)
1937	    case 1n++np 1n++mp:
1938	      %Equal.sym(Nat, Nat.add(r, 1n+mp), 1n+Nat.add(r, mp), add_succ(r, mp)) : le(Pair.snd(Nat, Nat, Nat.divmod.go(np, mp, d, 1n+r)), _)
1939	      internal_mod_go_le(np, mp, d, 1n+r)
1940	
1941	# A remainder is below its positive divisor: a % (1 + b) < 1 + b.
1942	law mod_lt:
1943	  for a: Nat
1944	  for b: Nat
1945	  lt(Nat.mod(a, 1n+b), 1n+b)
1946	
1947	def mod_lt(a, b):
1948	  +a = a
1949	  +b = b
1950	  %Equal.sym(Bool, Nat.is_lt(Nat.mod(a, 1n+b), 1n+b), Nat.is_le(1n+Nat.mod(a, 1n+b), 1n+b), is_lt_eq_succ_le(Nat.mod(a, 1n+b), 1n+b)) : {_ == True{} : Bool}
1951	  internal_mod_go_le(a, b, 0n, 0n)
1952	
1953	# A remainder never exceeds the dividend: a % b <= a.
1954	law mod_le:
1955	  for a: Nat
1956	  for b: Nat
1957	  le(Nat.mod(a, b), a)
1958	
1959	def mod_le(a, b):
1960	  match b:
1961	    case 0n:
1962	      le_refl(a)
1963	    case 1n++bp:
1964	      +a = a
1965	      +bp = bp
1966	      le_of_add_eq(Nat.mod(a, 1n+bp), Nat.mul(Nat.div(a, 1n+bp), 1n+bp), a, Equal.trans(Nat, Nat.add(Nat.mod(a, 1n+bp), Nat.mul(Nat.div(a, 1n+bp), 1n+bp)), Nat.add(Nat.mul(Nat.div(a, 1n+bp), 1n+bp), Nat.mod(a, 1n+bp)), a, add_comm(Nat.mod(a, 1n+bp), Nat.mul(Nat.div(a, 1n+bp), 1n+bp)), div_mod_eq(a, bp)))
1967	
1968	def internal_div_le_self_eq(+q: Nat, +bp: Nat, +m: Nat, -a: Nat, e: {Nat.add(Nat.mul(q, 1n+bp), m) == a : Nat}) -> {Nat.add(q, Nat.add(Nat.mul(bp, q), m)) == a : Nat}:
1969	  %e : {Nat.add(q, Nat.add(Nat.mul(bp, q), m)) == _ : Nat}
1970	  %mul_comm(1n+bp, q) : {Nat.add(q, Nat.add(Nat.mul(bp, q), m)) == Nat.add(_, m) : Nat}
1971	  Equal.sym(Nat, Nat.add(Nat.add(q, Nat.mul(bp, q)), m), Nat.add(q, Nat.add(Nat.mul(bp, q), m)), add_assoc(q, Nat.mul(bp, q), m))
1972	
1973	# A quotient never exceeds the dividend: a / b <= a.
1974	law div_le_self:
1975	  for a: Nat
1976	  for b: Nat
1977	  le(Nat.div(a, b), a)
1978	
1979	def div_le_self(a, b):
1980	  match b:
1981	    case 0n:
1982	      zero_le(a)
1983	    case 1n++bp:
1984	      +a = a
1985	      +bp = bp
1986	      le_of_add_eq(Nat.div(a, 1n+bp), Nat.add(Nat.mul(bp, Nat.div(a, 1n+bp)), Nat.mod(a, 1n+bp)), a, internal_div_le_self_eq(Nat.div(a, 1n+bp), bp, Nat.mod(a, 1n+bp), a, div_mod_eq(a, bp)))
1987	
1988	def internal_mod_go_small(n: Nat, -k: Nat, -d: Nat, +r: Nat) -> {Pair.snd(Nat, Nat, Nat.divmod.go(n, Nat.add(n, k), d, r)) == Nat.add(n, r) : Nat}:
1989	  match n:
1990	    case 0n:
1991	      {==}
1992	    case 1n++np:
1993	      %add_succ(np, r) : {Pair.snd(Nat, Nat, Nat.divmod.go(np, Nat.add(np, k), d, 1n+r)) == _ : Nat}
1994	      internal_mod_go_small(np, k, d, 1n+r)
1995	
1996	def internal_mod_eq_of_wit(+a: Nat, +b: Nat, w: &k:Nat -> {Nat.add(a, k) == b : Nat}) -> {Nat.mod(a, 1n+b) == a : Nat}:
1997	  match w:
1998	    case (+k, e):
1999	      %e : {Nat.mod(a, 1n+_) == a : Nat}
2000	      Equal.trans(Nat, Nat.mod(a, 1n+Nat.add(a, k)), Nat.add(a, 0n), a, internal_mod_go_small(a, k, 0n, 0n), add_zero(a))
Lines 1-2000 of 4906. More: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/nat.bend&start_line=2001