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