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	# Minimum is commutative.
741	law min_comm:
742	  for a: Nat
743	  for b: Nat
744	  {Nat.min(a, b) == Nat.min(b, a) : Nat}
745	
746	def min_comm(a, b):
747	  match a b:
748	    case 0n 0n:
749	      {==}
750	    case 0n 1n+q:
751	      {==}
752	    case 1n+p 0n:
753	      {==}
754	    case 1n++p 1n++q:
755	      %min_comm(p, q) : {1n+Nat.min(p, q) == 1n+_ : Nat}
756	      {==}
757	
758	# Maximum is commutative.
759	law max_comm:
760	  for a: Nat
761	  for b: Nat
762	  {Nat.max(a, b) == Nat.max(b, a) : Nat}
763	
764	def max_comm(a, b):
765	  match a b:
766	    case 0n 0n:
767	      {==}
768	    case 0n 1n+q:
769	      {==}
770	    case 1n+p 0n:
771	      {==}
772	    case 1n++p 1n++q:
773	      %max_comm(p, q) : {1n+Nat.max(p, q) == 1n+_ : Nat}
774	      {==}
775	
776	# The minimum of a natural and itself is itself.
777	law min_self:
778	  for a: Nat
779	  {Nat.min(a, a) == a : Nat}
780	
781	def min_self(a):
782	  match a:
783	    case 0n:
784	      {==}
785	    case 1n++p:
786	      %min_self(p) : {1n+Nat.min(p, p) == 1n+_ : Nat}
787	      {==}
788	
789	# The maximum of a natural and itself is itself.
790	law max_self:
791	  for a: Nat
792	  {Nat.max(a, a) == a : Nat}
793	
794	def max_self(a):
795	  match a:
796	    case 0n:
797	      {==}
798	    case 1n++p:
799	      %max_self(p) : {1n+Nat.max(p, p) == 1n+_ : Nat}
800	      {==}
801	
802	# The minimum with zero is zero: min(a, 0) = 0.
803	law min_zero:
804	  for a: Nat
805	  {Nat.min(a, 0n) == 0n : Nat}
806	
807	def min_zero(a):
808	  match a:
809	    case 0n:
810	      {==}
811	    case 1n+p:
812	      {==}
813	
814	# The minimum with zero is zero: min(0, a) = 0.
815	law zero_min:
816	  for a: Nat
817	  {Nat.min(0n, a) == 0n : Nat}
818	
819	def zero_min(a):
820	  match a:
821	    case 0n:
822	      {==}
823	    case 1n+p:
824	      {==}
825	
826	# Zero is an identity for maximum: max(a, 0) = a.
827	law max_zero:
828	  for a: Nat
829	  {Nat.max(a, 0n) == a : Nat}
830	
831	def max_zero(a):
832	  match a:
833	    case 0n:
834	      {==}
835	    case 1n+p:
836	      {==}
837	
838	# Zero is an identity for maximum: max(0, a) = a.
839	law zero_max:
840	  for a: Nat
841	  {Nat.max(0n, a) == a : Nat}
842	
843	def zero_max(a):
844	  match a:
845	    case 0n:
846	      {==}
847	    case 1n+p:
848	      {==}
849	
850	# Minimum is associative.
851	law min_assoc:
852	  for a: Nat
853	  for b: Nat
854	  for c: Nat
855	  {Nat.min(Nat.min(a, b), c) == Nat.min(a, Nat.min(b, c)) : Nat}
856	
857	def min_assoc(a, b, c):
858	  match a b c:
859	    case 0n _ _:
860	      {==}
861	    case 1n+p 0n _:
862	      {==}
863	    case 1n+p 1n+q 0n:
864	      {==}
865	    case 1n++p 1n++q 1n++r:
866	      %min_assoc(p, q, r) : {1n+Nat.min(Nat.min(p, q), r) == 1n+_ : Nat}
867	      {==}
868	
869	# Maximum is associative.
870	law max_assoc:
871	  for a: Nat
872	  for b: Nat
873	  for c: Nat
874	  {Nat.max(Nat.max(a, b), c) == Nat.max(a, Nat.max(b, c)) : Nat}
875	
876	def max_assoc(a, b, c):
877	  match a b c:
878	    case 0n _ _:
879	      {==}
880	    case 1n+p 0n _:
881	      {==}
882	    case 1n+p 1n+q 0n:
883	      {==}
884	    case 1n++p 1n++q 1n++r:
885	      %max_assoc(p, q, r) : {1n+Nat.max(Nat.max(p, q), r) == 1n+_ : Nat}
886	      {==}
887	
888	# The minimum plus the maximum is the sum: min(a, b) + max(a, b) = a + b.
889	law min_add_max:
890	  for a: Nat
891	  for b: Nat
892	  {Nat.add(Nat.min(a, b), Nat.max(a, b)) == Nat.add(a, b) : Nat}
893	
894	def min_add_max(a, b):
895	  match a b:
896	    case 0n 0n:
897	      {==}
898	    case 0n 1n+q:
899	      {==}
900	    case 1n++p 0n:
901	      %add_zero(p) : {1n+_ == 1n+Nat.add(p, 0n) : Nat}
902	      {==}
903	    case 1n++p 1n++q:
904	      %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}
905	      %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}
906	      %min_add_max(p, q) : {2n+Nat.add(Nat.min(p, q), Nat.max(p, q)) == 2n+_ : Nat}
907	      {==}
908	
909	# The minimum is at most its left argument.
910	law min_le_left:
911	  for a: Nat
912	  for b: Nat
913	  le(Nat.min(a, b), a)
914	
915	def min_le_left(a, b):
916	  match a b:
917	    case 0n 0n:
918	      {==}
919	    case 0n 1n+q:
920	      {==}
921	    case 1n+p 0n:
922	      {==}
923	    case 1n+p 1n+q:
924	      min_le_left(p, q)
925	
926	# The minimum is at most its right argument.
927	law min_le_right:
928	  for a: Nat
929	  for b: Nat
930	  le(Nat.min(a, b), b)
931	
932	def min_le_right(a, b):
933	  match a b:
934	    case 0n 0n:
935	      {==}
936	    case 0n 1n+q:
937	      {==}
938	    case 1n+p 0n:
939	      {==}
940	    case 1n+p 1n+q:
941	      min_le_right(p, q)
942	
943	# The left argument is at most the maximum.
944	law le_max_left:
945	  for a: Nat
946	  for b: Nat
947	  le(a, Nat.max(a, b))
948	
949	def le_max_left(a, b):
950	  match a b:
951	    case 0n 0n:
952	      {==}
953	    case 0n 1n+q:
954	      {==}
955	    case 1n+p 0n:
956	      le_refl(1n+p)
957	    case 1n+p 1n+q:
958	      le_max_left(p, q)
959	
960	# The right argument is at most the maximum.
961	law le_max_right:
962	  for a: Nat
963	  for b: Nat
964	  le(b, Nat.max(a, b))
965	
966	def le_max_right(a, b):
967	  match a b:
968	    case 0n 0n:
969	      {==}
970	    case 0n 1n+q:
971	      le_refl(1n+q)
972	    case 1n+p 0n:
973	      {==}
974	    case 1n+p 1n+q:
975	      le_max_right(p, q)
976	
977	# Any natural to the power zero is one.
978	law pow_zero:
979	  for -a: Nat
980	  {Nat.pow(a, 0n) == 1n : Nat}
981	
982	def pow_zero(a):
983	  {==}
984	
985	# A power with a successor exponent: a^(n+1) = a * a^n.
986	law pow_succ:
987	  for -a: Nat
988	  for -n: Nat
989	  {Nat.pow(a, 1n+n) == Nat.mul(a, Nat.pow(a, n)) : Nat}
990	
991	def pow_succ(a, n):
992	  {==}
993	
994	# Any natural to the power one is itself.
995	law pow_one:
996	  for a: Nat
997	  {Nat.pow(a, 1n) == a : Nat}
998	
999	def pow_one(a):
1000	  mul_one(a)
1001	
1002	# One to any power is one.
1003	law one_pow:
1004	  for n: Nat
1005	  {Nat.pow(1n, n) == 1n : Nat}
1006	
1007	def one_pow(n):
1008	  match n:
1009	    case 0n:
1010	      {==}
1011	    case 1n++p:
1012	      %Equal.sym(Nat, Nat.mul(1n, Nat.pow(1n, p)), Nat.pow(1n, p), one_mul(Nat.pow(1n, p))) : {_ == 1n : Nat}
1013	      one_pow(p)
1014	
1015	# Exponents add under multiplication: a^(m+n) = a^m * a^n.
1016	law pow_add:
1017	  for a: Nat
1018	  for m: Nat
1019	  for n: Nat
1020	  {Nat.pow(a, Nat.add(m, n)) == Nat.mul(Nat.pow(a, m), Nat.pow(a, n)) : Nat}
1021	
1022	def pow_add(a, m, n):
1023	  match m:
1024	    case 0n:
1025	      +a = a
1026	      +n = n
1027	      %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}
1028	      {==}
1029	    case 1n++p:
1030	      +a = a
1031	      +n = n
1032	      %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}
1033	      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)))
1034	
1035	# Doubling is adding a natural to itself.
1036	law double_eq_add:
1037	  for n: Nat
1038	  {Nat.double(n) == Nat.add(n, n) : Nat}
1039	
1040	def double_eq_add(n):
1041	  match n:
1042	    case 0n:
1043	      {==}
1044	    case 1n++p:
1045	      %Equal.sym(Nat, Nat.add(p, 1n+p), 1n+Nat.add(p, p), add_succ(p, p)) : {2n+Nat.double(p) == 1n+_ : Nat}
1046	      %double_eq_add(p) : {2n+Nat.double(p) == 2n+_ : Nat}
1047	      {==}
1048	
1049	# Every natural tests equal to itself.
1050	law is_eq_refl:
1051	  for n: Nat
1052	  {Nat.is_eq(n, n) == True{} : Bool}
1053	
1054	def is_eq_refl(n):
1055	  match n:
1056	    case 0n:
1057	      {==}
1058	    case 1n+p:
1059	      is_eq_refl(p)
1060	
1061	# The equality test is symmetric.
1062	law is_eq_comm:
1063	  for a: Nat
1064	  for b: Nat
1065	  {Nat.is_eq(a, b) == Nat.is_eq(b, a) : Bool}
1066	
1067	def is_eq_comm(a, b):
1068	  match a b:
1069	    case 0n 0n:
1070	      {==}
1071	    case 0n 1n+q:
1072	      {==}
1073	    case 1n+p 0n:
1074	      {==}
1075	    case 1n++p 1n++q:
1076	      %is_eq_comm(p, q) : {Nat.is_eq(p, q) == _ : Bool}
1077	      {==}
1078	
1079	# If the equality test says true, the naturals are equal.
1080	law eq_of_is_eq:
1081	  for a: Nat
1082	  for b: Nat
1083	  for h: {Nat.is_eq(a, b) == True{} : Bool}
1084	  {a == b : Nat}
1085	
1086	def eq_of_is_eq(a, b, h):
1087	  match a b:
1088	    case 0n 0n:
1089	      {==}
1090	    case 0n 1n+q:
1091	      Empty.absurd({0n == 1n+q : Nat}, internal_false_ne_true(h))
1092	    case 1n+p 0n:
1093	      Empty.absurd({1n+p == 0n : Nat}, internal_false_ne_true(h))
1094	    case 1n++p 1n++q:
1095	      %eq_of_is_eq(p, q, h) : {1n+p == 1n+_ : Nat}
1096	      {==}
1097	
1098	# A >= b tests the same as b <= a.
1099	law is_ge_eq_is_le:
1100	  for a: Nat
1101	  for b: Nat
1102	  {Nat.is_ge(a, b) == Nat.is_le(b, a) : Bool}
1103	
1104	def is_ge_eq_is_le(a, b):
1105	  match a b:
1106	    case 0n 0n:
1107	      {==}
1108	    case 0n 1n+q:
1109	      {==}
1110	    case 1n+p 0n:
1111	      {==}
1112	    case 1n++p 1n++q:
1113	      %is_ge_eq_is_le(p, q) : {Nat.is_ge(p, q) == _ : Bool}
1114	      {==}
1115	
1116	# A > b tests the same as b < a.
1117	law is_gt_eq_is_lt:
1118	  for a: Nat
1119	  for b: Nat
1120	  {Nat.is_gt(a, b) == Nat.is_lt(b, a) : Bool}
1121	
1122	def is_gt_eq_is_lt(a, b):
1123	  match a b:
1124	    case 0n 0n:
1125	      {==}
1126	    case 0n 1n+q:
1127	      {==}
1128	    case 1n+p 0n:
1129	      {==}
1130	    case 1n++p 1n++q:
1131	      %is_gt_eq_is_lt(p, q) : {Nat.is_gt(p, q) == _ : Bool}
1132	      {==}
1133	
1134	# A < b tests the same as a + 1 <= b.
1135	law is_lt_eq_succ_le:
1136	  for a: Nat
1137	  for b: Nat
1138	  {Nat.is_lt(a, b) == Nat.is_le(1n+a, b) : Bool}
1139	
1140	def is_lt_eq_succ_le(a, b):
1141	  match a b:
1142	    case 0n 0n:
1143	      {==}
1144	    case 0n 1n+q:
1145	      match q:
1146	        case 0n:
1147	          {==}
1148	        case 1n+r:
1149	          {==}
1150	    case 1n+p 0n:
1151	      {==}
1152	    case 1n+p 1n+q:
1153	      is_lt_eq_succ_le(p, q)
1154	
1155	# Not (a <= b) tests the same as b < a.
1156	law not_is_le:
1157	  for a: Nat
1158	  for b: Nat
1159	  {Bool.not(Nat.is_le(a, b)) == Nat.is_lt(b, a) : Bool}
1160	
1161	def not_is_le(a, b):
1162	  match a b:
1163	    case 0n 0n:
1164	      {==}
1165	    case 0n 1n+q:
1166	      {==}
1167	    case 1n+p 0n:
1168	      {==}
1169	    case 1n+p 1n+q:
1170	      not_is_le(p, q)
1171	
1172	# Not (a < b) tests the same as b <= a.
1173	law not_is_lt:
1174	  for a: Nat
1175	  for b: Nat
1176	  {Bool.not(Nat.is_lt(a, b)) == Nat.is_le(b, a) : Bool}
1177	
1178	def not_is_lt(a, b):
1179	  match a b:
1180	    case 0n 0n:
1181	      {==}
1182	    case 0n 1n+q:
1183	      {==}
1184	    case 1n+p 0n:
1185	      {==}
1186	    case 1n+p 1n+q:
1187	      not_is_lt(p, q)
1188	
1189	# Every natural is less than its successor: n < n + 1.
1190	law lt_succ_self:
1191	  for n: Nat
1192	  lt(n, 1n+n)
1193	
1194	def lt_succ_self(n):
1195	  match n:
1196	    case 0n:
1197	      {==}
1198	    case 1n+p:
1199	      lt_succ_self(p)
1200	
1201	# The successor preserves the order: a <= b implies a + 1 <= b + 1.
1202	law succ_le_succ:
1203	  for -a: Nat
1204	  for -b: Nat
1205	  for h: le(a, b)
1206	  le(1n+a, 1n+b)
1207	
1208	def succ_le_succ(a, b, h):
1209	  h
1210	
1211	# The order of successors is the order of the naturals: a + 1 <= b + 1 implies a <= b.
1212	law le_of_succ_le_succ:
1213	  for -a: Nat
1214	  for -b: Nat
1215	  for h: le(1n+a, 1n+b)
1216	  le(a, b)
1217	
1218	def le_of_succ_le_succ(a, b, h):
1219	  h
1220	
1221	# A < b and b <= c imply a < c.
1222	law lt_of_lt_of_le:
1223	  for a: Nat
1224	  for b: Nat
1225	  for c: Nat
1226	  for ab: lt(a, b)
1227	  for bc: le(b, c)
1228	  lt(a, c)
1229	
1230	def lt_of_lt_of_le(a, b, c, ab, bc):
1231	  match a b c:
1232	    case 0n 0n _:
1233	      Empty.absurd(lt(0n, c), internal_false_ne_true(ab))
1234	    case 0n 1n+q 0n:
1235	      Empty.absurd(lt(0n, 0n), internal_false_ne_true(bc))
1236	    case 0n 1n+q 1n+r:
1237	      {==}
1238	    case 1n+p 0n _:
1239	      Empty.absurd(lt(1n+p, c), internal_false_ne_true(ab))
1240	    case 1n+p 1n+q 0n:
1241	      Empty.absurd(lt(1n+p, 0n), internal_false_ne_true(bc))
1242	    case 1n+p 1n+q 1n+r:
1243	      lt_of_lt_of_le(p, q, r, ab, bc)
1244	
1245	# A <= b and b < c imply a < c.
1246	law lt_of_le_of_lt:
1247	  for a: Nat
1248	  for b: Nat
1249	  for c: Nat
1250	  for ab: le(a, b)
1251	  for bc: lt(b, c)
1252	  lt(a, c)
1253	
1254	def lt_of_le_of_lt(a, b, c, ab, bc):
1255	  match a b c:
1256	    case 0n 0n 0n:
1257	      Empty.absurd(lt(0n, 0n), internal_false_ne_true(bc))
1258	    case 0n 1n+q 0n:
1259	      Empty.absurd(lt(0n, 0n), internal_false_ne_true(bc))
1260	    case 0n _ 1n+r:
1261	      {==}
1262	    case 1n+p 0n _:
1263	      Empty.absurd(lt(1n+p, c), internal_false_ne_true(ab))
1264	    case 1n+p 1n+q 0n:
1265	      Empty.absurd(lt(1n+p, 0n), internal_false_ne_true(bc))
1266	    case 1n+p 1n+q 1n+r:
1267	      lt_of_le_of_lt(p, q, r, ab, bc)
1268	
1269	# Adding on the left preserves the order: a <= b implies k + a <= k + b.
1270	law add_le_add_left:
1271	  for -a: Nat
1272	  for -b: Nat
1273	  for k: Nat
1274	  for h: le(a, b)
1275	  le(Nat.add(k, a), Nat.add(k, b))
1276	
1277	def add_le_add_left(a, b, k, h):
1278	  match k:
1279	    case 0n:
1280	      h
1281	    case 1n+p:
1282	      add_le_add_left(a, b, p, h)
1283	
1284	# The only natural at most zero is zero.
1285	law le_zero_eq:
1286	  for n: Nat
1287	  for h: le(n, 0n)
1288	  {n == 0n : Nat}
1289	
1290	def le_zero_eq(n, h):
1291	  match n:
1292	    case 0n:
1293	      {==}
1294	    case 1n+p:
1295	      Empty.absurd({1n+p == 0n : Nat}, internal_false_ne_true(h))
1296	
1297	# No natural is less than zero.
1298	law lt_zero:
1299	  for n: Nat
1300	  lt(n, 0n) -> Empty
1301	
1302	def lt_zero(n):
1303	  match n:
1304	    case 0n:
1305	      h => internal_false_ne_true(h)
1306	    case 1n+p:
1307	      h => internal_false_ne_true(h)
1308	
1309	# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
1310	
1311	# Zero is a right identity for addition: x + 0 = x, reversed to rewrite toward the simple side.
1312	law add_zero_sym:
1313	  for x: Nat
1314	  {x == Nat.add(x, 0n) : Nat}
1315	
1316	def add_zero_sym(x):
1317	  Equal.sym(Nat, Nat.add(x, 0n), x, add_zero(x))
1318	
1319	# Zero is a left identity for addition: 0 + x = x, reversed to rewrite toward the simple side.
1320	law zero_add_sym:
1321	  for -x: Nat
1322	  {x == Nat.add(0n, x) : Nat}
1323	
1324	def zero_add_sym(x):
1325	  Equal.sym(Nat, Nat.add(0n, x), x, zero_add(x))
1326	
1327	# Adding a successor on the right: n + (m + 1) = (n + m) + 1, reversed to rewrite toward the simple side.
1328	law add_succ_sym:
1329	  for n: Nat
1330	  for -m: Nat
1331	  {1n+Nat.add(n, m) == Nat.add(n, 1n+m) : Nat}
1332	
1333	def add_succ_sym(n, m):
1334	  Equal.sym(Nat, Nat.add(n, 1n+m), 1n+Nat.add(n, m), add_succ(n, m))
1335	
1336	# Adding a successor on the left: (n + 1) + m = (n + m) + 1, reversed to rewrite toward the simple side.
1337	law succ_add_sym:
1338	  for -n: Nat
1339	  for -m: Nat
1340	  {1n+Nat.add(n, m) == Nat.add(1n+n, m) : Nat}
1341	
1342	def succ_add_sym(n, m):
1343	  Equal.sym(Nat, Nat.add(1n+n, m), 1n+Nat.add(n, m), succ_add(n, m))
1344	
1345	# Addition is commutative: n + m = m + n, reversed to rewrite toward the simple side.
1346	law add_comm_sym:
1347	  for n: Nat
1348	  for m: Nat
1349	  {Nat.add(m, n) == Nat.add(n, m) : Nat}
1350	
1351	def add_comm_sym(n, m):
1352	  Equal.sym(Nat, Nat.add(n, m), Nat.add(m, n), add_comm(n, m))
1353	
1354	# Addition is associative: (a + b) + c = a + (b + c), reversed to rewrite toward the simple side.
1355	law add_assoc_sym:
1356	  for a: Nat
1357	  for -b: Nat
1358	  for -c: Nat
1359	  {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, b), c) : Nat}
1360	
1361	def add_assoc_sym(a, b, c):
1362	  Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(a, Nat.add(b, c)), add_assoc(a, b, c))
1363	
1364	# Left commutativity of addition: a + (b + c) = b + (a + c), reversed to rewrite toward the simple side.
1365	law add_left_comm_sym:
1366	  for a: Nat
1367	  for b: Nat
1368	  for -c: Nat
1369	  {Nat.add(b, Nat.add(a, c)) == Nat.add(a, Nat.add(b, c)) : Nat}
1370	
1371	def add_left_comm_sym(a, b, c):
1372	  Equal.sym(Nat, Nat.add(a, Nat.add(b, c)), Nat.add(b, Nat.add(a, c)), add_left_comm(a, b, c))
1373	
1374	# Right commutativity of addition: (a + b) + c = (a + c) + b, reversed to rewrite toward the simple side.
1375	law add_right_comm_sym:
1376	  for a: Nat
1377	  for b: Nat
1378	  for c: Nat
1379	  {Nat.add(Nat.add(a, c), b) == Nat.add(Nat.add(a, b), c) : Nat}
1380	
1381	def add_right_comm_sym(a, b, c):
1382	  Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(Nat.add(a, c), b), add_right_comm(a, b, c))
1383	
1384	# Four-way regrouping of a sum: (a + b) + (c + d) = (a + c) + (b + d), reversed to rewrite toward the simple side.
1385	law add_add_add_comm_sym:
1386	  for a: Nat
1387	  for b: Nat
1388	  for c: Nat
1389	  for -d: Nat
1390	  {Nat.add(Nat.add(a, c), Nat.add(b, d)) == Nat.add(Nat.add(a, b), Nat.add(c, d)) : Nat}
1391	
1392	def add_add_add_comm_sym(a, b, c, d):
1393	  Equal.sym(Nat, Nat.add(Nat.add(a, b), Nat.add(c, d)), Nat.add(Nat.add(a, c), Nat.add(b, d)), add_add_add_comm(a, b, c, d))
1394	
1395	# Zero absorbs multiplication on the right: x * 0 = 0, reversed to rewrite toward the simple side.
1396	law mul_zero_sym:
1397	  for x: Nat
1398	  {0n == Nat.mul(x, 0n) : Nat}
1399	
1400	def mul_zero_sym(x):
1401	  Equal.sym(Nat, Nat.mul(x, 0n), 0n, mul_zero(x))
1402	
1403	# Zero absorbs multiplication on the left: 0 * x = 0, reversed to rewrite toward the simple side.
1404	law zero_mul_sym:
1405	  for -x: Nat
1406	  {0n == Nat.mul(0n, x) : Nat}
1407	
1408	def zero_mul_sym(x):
1409	  Equal.sym(Nat, Nat.mul(0n, x), 0n, zero_mul(x))
1410	
1411	# One is a right identity for multiplication: x * 1 = x, reversed to rewrite toward the simple side.
1412	law mul_one_sym:
1413	  for x: Nat
1414	  {x == Nat.mul(x, 1n) : Nat}
1415	
1416	def mul_one_sym(x):
1417	  Equal.sym(Nat, Nat.mul(x, 1n), x, mul_one(x))
1418	
1419	# One is a left identity for multiplication: 1 * x = x, reversed to rewrite toward the simple side.
1420	law one_mul_sym:
1421	  for x: Nat
1422	  {x == Nat.mul(1n, x) : Nat}
1423	
1424	def one_mul_sym(x):
1425	  Equal.sym(Nat, Nat.mul(1n, x), x, one_mul(x))
1426	
1427	# Multiplying by a successor on the right: n * (m + 1) = n * m + n, reversed to rewrite toward the simple side.
1428	law mul_succ_sym:
1429	  for n: Nat
1430	  for m: Nat
1431	  {Nat.add(Nat.mul(n, m), n) == Nat.mul(n, 1n+m) : Nat}
1432	
1433	def mul_succ_sym(n, m):
1434	  Equal.sym(Nat, Nat.mul(n, 1n+m), Nat.add(Nat.mul(n, m), n), mul_succ(n, m))
1435	
1436	# Multiplying by a successor on the left: (n + 1) * m = n * m + m, reversed to rewrite toward the simple side.
1437	law succ_mul_sym:
1438	  for n: Nat
1439	  for m: Nat
1440	  {Nat.add(Nat.mul(n, m), m) == Nat.mul(1n+n, m) : Nat}
1441	
1442	def succ_mul_sym(n, m):
1443	  Equal.sym(Nat, Nat.mul(1n+n, m), Nat.add(Nat.mul(n, m), m), succ_mul(n, m))
1444	
1445	# Multiplication is commutative: n * m = m * n, reversed to rewrite toward the simple side.
1446	law mul_comm_sym:
1447	  for n: Nat
1448	  for m: Nat
1449	  {Nat.mul(m, n) == Nat.mul(n, m) : Nat}
1450	
1451	def mul_comm_sym(n, m):
1452	  Equal.sym(Nat, Nat.mul(n, m), Nat.mul(m, n), mul_comm(n, m))
1453	
1454	# Multiplication distributes over addition on the right: (a + b) * c = a * c + b * c, reversed to rewrite toward the simple side.
1455	law add_mul_sym:
1456	  for a: Nat
1457	  for -b: Nat
1458	  for c: Nat
1459	  {Nat.add(Nat.mul(a, c), Nat.mul(b, c)) == Nat.mul(Nat.add(a, b), c) : Nat}
1460	
1461	def add_mul_sym(a, b, c):
1462	  Equal.sym(Nat, Nat.mul(Nat.add(a, b), c), Nat.add(Nat.mul(a, c), Nat.mul(b, c)), add_mul(a, b, c))
1463	
1464	# Multiplication distributes over addition on the left: a * (b + c) = a * b + a * c, reversed to rewrite toward the simple side.
1465	law mul_add_sym:
1466	  for a: Nat
1467	  for b: Nat
1468	  for c: Nat
1469	  {Nat.add(Nat.mul(a, b), Nat.mul(a, c)) == Nat.mul(a, Nat.add(b, c)) : Nat}
1470	
1471	def mul_add_sym(a, b, c):
1472	  Equal.sym(Nat, Nat.mul(a, Nat.add(b, c)), Nat.add(Nat.mul(a, b), Nat.mul(a, c)), mul_add(a, b, c))
1473	
1474	# Multiplication is associative: (a * b) * c = a * (b * c), reversed to rewrite toward the simple side.
1475	law mul_assoc_sym:
1476	  for a: Nat
1477	  for b: Nat
1478	  for c: Nat
1479	  {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(Nat.mul(a, b), c) : Nat}
1480	
1481	def mul_assoc_sym(a, b, c):
1482	  Equal.sym(Nat, Nat.mul(Nat.mul(a, b), c), Nat.mul(a, Nat.mul(b, c)), mul_assoc(a, b, c))
1483	
1484	# Subtracting zero changes nothing: n - 0 = n, reversed to rewrite toward the simple side.
1485	law sub_zero_sym:
1486	  for n: Nat
1487	  {n == Nat.sub(n, 0n) : Nat}
1488	
1489	def sub_zero_sym(n):
1490	  Equal.sym(Nat, Nat.sub(n, 0n), n, sub_zero(n))
1491	
1492	# Truncated subtraction from zero is zero: 0 - n = 0, reversed to rewrite toward the simple side.
1493	law zero_sub_sym:
1494	  for n: Nat
1495	  {0n == Nat.sub(0n, n) : Nat}
1496	
1497	def zero_sub_sym(n):
1498	  Equal.sym(Nat, Nat.sub(0n, n), 0n, zero_sub(n))
1499	
1500	# A natural minus itself is zero: n - n = 0, reversed to rewrite toward the simple side.
1501	law sub_self_sym:
1502	  for n: Nat
1503	  {0n == Nat.sub(n, n) : Nat}
1504	
1505	def sub_self_sym(n):
1506	  Equal.sym(Nat, Nat.sub(n, n), 0n, sub_self(n))
1507	
1508	# Subtracting successors: (n + 1) - (m + 1) = n - m, reversed to rewrite toward the simple side.
1509	law succ_sub_succ_sym:
1510	  for -n: Nat
1511	  for -m: Nat
1512	  {Nat.sub(n, m) == Nat.sub(1n+n, 1n+m) : Nat}
1513	
1514	def succ_sub_succ_sym(n, m):
1515	  Equal.sym(Nat, Nat.sub(1n+n, 1n+m), Nat.sub(n, m), succ_sub_succ(n, m))
1516	
1517	# Adding then subtracting m cancels: (n + m) - m = n, reversed to rewrite toward the simple side.
1518	law add_sub_cancel_sym:
1519	  for n: Nat
1520	  for m: Nat
1521	  {n == Nat.sub(Nat.add(n, m), m) : Nat}
1522	
1523	def add_sub_cancel_sym(n, m):
1524	  Equal.sym(Nat, Nat.sub(Nat.add(n, m), m), n, add_sub_cancel(n, m))
1525	
1526	# Adding then subtracting n cancels: (n + m) - n = m, reversed to rewrite toward the simple side.
1527	law add_sub_cancel_left_sym:
1528	  for n: Nat
1529	  for m: Nat
1530	  {m == Nat.sub(Nat.add(n, m), n) : Nat}
1531	
1532	def add_sub_cancel_left_sym(n, m):
1533	  Equal.sym(Nat, Nat.sub(Nat.add(n, m), n), m, add_sub_cancel_left(n, m))
1534	
1535	# Subtracting twice is subtracting the sum: (n - m) - k = n - (m + k), reversed to rewrite toward the simple side.
1536	law sub_sub_sym:
1537	  for n: Nat
1538	  for m: Nat
1539	  for k: Nat
1540	  {Nat.sub(n, Nat.add(m, k)) == Nat.sub(Nat.sub(n, m), k) : Nat}
1541	
1542	def sub_sub_sym(n, m, k):
1543	  Equal.sym(Nat, Nat.sub(Nat.sub(n, m), k), Nat.sub(n, Nat.add(m, k)), sub_sub(n, m, k))
1544	
1545	# Minimum is commutative, reversed to rewrite toward the simple side.
1546	law min_comm_sym:
1547	  for a: Nat
1548	  for b: Nat
1549	  {Nat.min(b, a) == Nat.min(a, b) : Nat}
1550	
1551	def min_comm_sym(a, b):
1552	  Equal.sym(Nat, Nat.min(a, b), Nat.min(b, a), min_comm(a, b))
1553	
1554	# Maximum is commutative, reversed to rewrite toward the simple side.
1555	law max_comm_sym:
1556	  for a: Nat
1557	  for b: Nat
1558	  {Nat.max(b, a) == Nat.max(a, b) : Nat}
1559	
1560	def max_comm_sym(a, b):
1561	  Equal.sym(Nat, Nat.max(a, b), Nat.max(b, a), max_comm(a, b))
1562	
1563	# The minimum of a natural and itself is itself, reversed to rewrite toward the simple side.
1564	law min_self_sym:
1565	  for a: Nat
1566	  {a == Nat.min(a, a) : Nat}
1567	
1568	def min_self_sym(a):
1569	  Equal.sym(Nat, Nat.min(a, a), a, min_self(a))
1570	
1571	# The maximum of a natural and itself is itself, reversed to rewrite toward the simple side.
1572	law max_self_sym:
1573	  for a: Nat
1574	  {a == Nat.max(a, a) : Nat}
1575	
1576	def max_self_sym(a):
1577	  Equal.sym(Nat, Nat.max(a, a), a, max_self(a))
1578	
1579	# The minimum with zero is zero: min(a, 0) = 0, reversed to rewrite toward the simple side.
1580	law min_zero_sym:
1581	  for a: Nat
1582	  {0n == Nat.min(a, 0n) : Nat}
1583	
1584	def min_zero_sym(a):
1585	  Equal.sym(Nat, Nat.min(a, 0n), 0n, min_zero(a))
1586	
1587	# The minimum with zero is zero: min(0, a) = 0, reversed to rewrite toward the simple side.
1588	law zero_min_sym:
1589	  for a: Nat
1590	  {0n == Nat.min(0n, a) : Nat}
1591	
1592	def zero_min_sym(a):
1593	  Equal.sym(Nat, Nat.min(0n, a), 0n, zero_min(a))
1594	
1595	# Zero is an identity for maximum: max(a, 0) = a, reversed to rewrite toward the simple side.
1596	law max_zero_sym:
1597	  for a: Nat
1598	  {a == Nat.max(a, 0n) : Nat}
1599	
1600	def max_zero_sym(a):
1601	  Equal.sym(Nat, Nat.max(a, 0n), a, max_zero(a))
1602	
1603	# Zero is an identity for maximum: max(0, a) = a, reversed to rewrite toward the simple side.
1604	law zero_max_sym:
1605	  for a: Nat
1606	  {a == Nat.max(0n, a) : Nat}
1607	
1608	def zero_max_sym(a):
1609	  Equal.sym(Nat, Nat.max(0n, a), a, zero_max(a))
1610	
1611	# Minimum is associative, reversed to rewrite toward the simple side.
1612	law min_assoc_sym:
1613	  for a: Nat
1614	  for b: Nat
1615	  for c: Nat
1616	  {Nat.min(a, Nat.min(b, c)) == Nat.min(Nat.min(a, b), c) : Nat}
1617	
1618	def min_assoc_sym(a, b, c):
1619	  Equal.sym(Nat, Nat.min(Nat.min(a, b), c), Nat.min(a, Nat.min(b, c)), min_assoc(a, b, c))
1620	
1621	# Maximum is associative, reversed to rewrite toward the simple side.
1622	law max_assoc_sym:
1623	  for a: Nat
1624	  for b: Nat
1625	  for c: Nat
1626	  {Nat.max(a, Nat.max(b, c)) == Nat.max(Nat.max(a, b), c) : Nat}
1627	
1628	def max_assoc_sym(a, b, c):
1629	  Equal.sym(Nat, Nat.max(Nat.max(a, b), c), Nat.max(a, Nat.max(b, c)), max_assoc(a, b, c))
1630	
1631	# The minimum plus the maximum is the sum: min(a, b) + max(a, b) = a + b, reversed to rewrite toward the simple side.
1632	law min_add_max_sym:
1633	  for a: Nat
1634	  for b: Nat
1635	  {Nat.add(a, b) == Nat.add(Nat.min(a, b), Nat.max(a, b)) : Nat}
1636	
1637	def min_add_max_sym(a, b):
1638	  Equal.sym(Nat, Nat.add(Nat.min(a, b), Nat.max(a, b)), Nat.add(a, b), min_add_max(a, b))
1639	
1640	# Any natural to the power zero is one, reversed to rewrite toward the simple side.
1641	law pow_zero_sym:
1642	  for -a: Nat
1643	  {1n == Nat.pow(a, 0n) : Nat}
1644	
1645	def pow_zero_sym(a):
1646	  Equal.sym(Nat, Nat.pow(a, 0n), 1n, pow_zero(a))
1647	
1648	# A power with a successor exponent: a^(n+1) = a * a^n, reversed to rewrite toward the simple side.
1649	law pow_succ_sym:
1650	  for -a: Nat
1651	  for -n: Nat
1652	  {Nat.mul(a, Nat.pow(a, n)) == Nat.pow(a, 1n+n) : Nat}
1653	
1654	def pow_succ_sym(a, n):
1655	  Equal.sym(Nat, Nat.pow(a, 1n+n), Nat.mul(a, Nat.pow(a, n)), pow_succ(a, n))
1656	
1657	# Any natural to the power one is itself, reversed to rewrite toward the simple side.
1658	law pow_one_sym:
1659	  for a: Nat
1660	  {a == Nat.pow(a, 1n) : Nat}
1661	
1662	def pow_one_sym(a):
1663	  Equal.sym(Nat, Nat.pow(a, 1n), a, pow_one(a))
1664	
1665	# One to any power is one, reversed to rewrite toward the simple side.
1666	law one_pow_sym:
1667	  for n: Nat
1668	  {1n == Nat.pow(1n, n) : Nat}
1669	
1670	def one_pow_sym(n):
1671	  Equal.sym(Nat, Nat.pow(1n, n), 1n, one_pow(n))
1672	
1673	# Exponents add under multiplication: a^(m+n) = a^m * a^n, reversed to rewrite toward the simple side.
1674	law pow_add_sym:
1675	  for a: Nat
1676	  for m: Nat
1677	  for n: Nat
1678	  {Nat.mul(Nat.pow(a, m), Nat.pow(a, n)) == Nat.pow(a, Nat.add(m, n)) : Nat}
1679	
1680	def pow_add_sym(a, m, n):
1681	  Equal.sym(Nat, Nat.pow(a, Nat.add(m, n)), Nat.mul(Nat.pow(a, m), Nat.pow(a, n)), pow_add(a, m, n))
1682	
1683	# Doubling is adding a natural to itself, reversed to rewrite toward the simple side.
1684	law double_eq_add_sym:
1685	  for n: Nat
1686	  {Nat.add(n, n) == Nat.double(n) : Nat}
1687	
1688	def double_eq_add_sym(n):
1689	  Equal.sym(Nat, Nat.double(n), Nat.add(n, n), double_eq_add(n))
1690	
1691	# Every natural tests equal to itself, reversed to rewrite toward the simple side.
1692	law is_eq_refl_sym:
1693	  for n: Nat
1694	  {True{} == Nat.is_eq(n, n) : Bool}
1695	
1696	def is_eq_refl_sym(n):
1697	  Equal.sym(Bool, Nat.is_eq(n, n), True{}, is_eq_refl(n))
1698	
1699	# The equality test is symmetric, reversed to rewrite toward the simple side.
1700	law is_eq_comm_sym:
1701	  for a: Nat
1702	  for b: Nat
1703	  {Nat.is_eq(b, a) == Nat.is_eq(a, b) : Bool}
1704	
1705	def is_eq_comm_sym(a, b):
1706	  Equal.sym(Bool, Nat.is_eq(a, b), Nat.is_eq(b, a), is_eq_comm(a, b))
1707	
1708	# A >= b tests the same as b <= a, reversed to rewrite toward the simple side.
1709	law is_ge_eq_is_le_sym:
1710	  for a: Nat
1711	  for b: Nat
1712	  {Nat.is_le(b, a) == Nat.is_ge(a, b) : Bool}
1713	
1714	def is_ge_eq_is_le_sym(a, b):
1715	  Equal.sym(Bool, Nat.is_ge(a, b), Nat.is_le(b, a), is_ge_eq_is_le(a, b))
1716	
1717	# A > b tests the same as b < a, reversed to rewrite toward the simple side.
1718	law is_gt_eq_is_lt_sym:
1719	  for a: Nat
1720	  for b: Nat
1721	  {Nat.is_lt(b, a) == Nat.is_gt(a, b) : Bool}
1722	
1723	def is_gt_eq_is_lt_sym(a, b):
1724	  Equal.sym(Bool, Nat.is_gt(a, b), Nat.is_lt(b, a), is_gt_eq_is_lt(a, b))
1725	
1726	# A < b tests the same as a + 1 <= b, reversed to rewrite toward the simple side.
1727	law is_lt_eq_succ_le_sym:
1728	  for a: Nat
1729	  for b: Nat
1730	  {Nat.is_le(1n+a, b) == Nat.is_lt(a, b) : Bool}
1731	
1732	def is_lt_eq_succ_le_sym(a, b):
1733	  Equal.sym(Bool, Nat.is_lt(a, b), Nat.is_le(1n+a, b), is_lt_eq_succ_le(a, b))
1734	
1735	# Not (a <= b) tests the same as b < a, reversed to rewrite toward the simple side.
1736	law not_is_le_sym:
1737	  for a: Nat
1738	  for b: Nat
1739	  {Nat.is_lt(b, a) == Bool.not(Nat.is_le(a, b)) : Bool}
1740	
1741	def not_is_le_sym(a, b):
1742	  Equal.sym(Bool, Bool.not(Nat.is_le(a, b)), Nat.is_lt(b, a), not_is_le(a, b))
1743	
1744	# Not (a < b) tests the same as b <= a, reversed to rewrite toward the simple side.
1745	law not_is_lt_sym:
1746	  for a: Nat
1747	  for b: Nat
1748	  {Nat.is_le(b, a) == Bool.not(Nat.is_lt(a, b)) : Bool}
1749	
1750	def not_is_lt_sym(a, b):
1751	  Equal.sym(Bool, Bool.not(Nat.is_lt(a, b)), Nat.is_le(b, a), not_is_lt(a, b))