1	import Base
2	
3	# Zero is a right identity for addition: x + 0 = x.
4	law add_zero:
5	  for x: Nat
6	  {Nat.add(x, 0n) == x : Nat}
7	
8	def add_zero(x):
9	  match x:
10	    case 0n:
11	      {==}
12	    case 1n+p:
13	      %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
14	      {==}
15	
16	# Zero is a left identity for addition: 0 + x = x.
17	law zero_add:
18	  for -x: Nat
19	  {Nat.add(0n, x) == x : Nat}
20	
21	def zero_add(x):
22	  {==}
23	
24	# Adding a successor on the right: n + (m + 1) = (n + m) + 1.
25	law add_succ:
26	  for n: Nat
27	  for -m: Nat
28	  {Nat.add(n, 1n+m) == 1n+Nat.add(n, m) : Nat}
29	
30	def add_succ(n, m):
31	  match n:
32	    case 0n:
33	      {==}
34	    case 1n+p:
35	      %add_succ(p, m) : {1n+Nat.add(p, 1n+m) == 1n+_ : Nat}
36	      {==}
37	
38	# Adding a successor on the left: (n + 1) + m = (n + m) + 1.
39	law succ_add:
40	  for -n: Nat
41	  for -m: Nat
42	  {Nat.add(1n+n, m) == 1n+Nat.add(n, m) : Nat}
43	
44	def succ_add(n, m):
45	  {==}
46	
47	# Addition is commutative: n + m = m + n.
48	law add_comm:
49	  for n: Nat
50	  for m: Nat
51	  {Nat.add(n, m) == Nat.add(m, n) : Nat}
52	
53	def add_comm(n, m):
54	  match n m:
55	    case 0n 0n:
56	      {==}
57	    case 0n 1n+q:
58	      %add_zero(q) : {1n+_ == 1n+Nat.add(q, 0n) : Nat}
59	      {==}
60	    case 1n+p 0n:
61	      %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
62	      {==}
63	    case 1n++p 1n++q:
64	      %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}
65	      %Equal.sym(Nat, Nat.add(q, 1n+p), 1n+Nat.add(q, p), add_succ(q, p)) : {2n+Nat.add(p, q) == 1n+_ : Nat}
66	      %add_comm(p, q) : {2n+Nat.add(p, q) == 2n+_ : Nat}
67	      {==}
68	
69	# Addition is associative: (a + b) + c = a + (b + c).
70	law add_assoc:
71	  for a: Nat
72	  for -b: Nat
73	  for -c: Nat
74	  {Nat.add(Nat.add(a, b), c) == Nat.add(a, Nat.add(b, c)) : Nat}
75	
76	def add_assoc(a, b, c):
77	  match a:
78	    case 0n:
79	      {==}
80	    case 1n+p:
81	      %add_assoc(p, b, c) : {1n+Nat.add(Nat.add(p, b), c) == 1n+_ : Nat}
82	      {==}
83	
84	# Left commutativity of addition: a + (b + c) = b + (a + c).
85	law add_left_comm:
86	  for a: Nat
87	  for b: Nat
88	  for -c: Nat
89	  {Nat.add(a, Nat.add(b, c)) == Nat.add(b, Nat.add(a, c)) : Nat}
90	
91	def add_left_comm(a, b, c):
92	  match a:
93	    case 0n:
94	      {==}
95	    case 1n+p:
96	      +b = b
97	      %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}
98	      %add_left_comm(p, b, c) : {1n+Nat.add(p, Nat.add(b, c)) == 1n+_ : Nat}
99	      {==}
100	
101	# Right commutativity of addition: (a + b) + c = (a + c) + b.
102	law add_right_comm:
103	  for a: Nat
104	  for b: Nat
105	  for c: Nat
106	  {Nat.add(Nat.add(a, b), c) == Nat.add(Nat.add(a, c), b) : Nat}
107	
108	def add_right_comm(a, b, c):
109	  match a:
110	    case 0n:
111	      add_comm(b, c)
112	    case 1n+p:
113	      %add_right_comm(p, b, c) : {1n+Nat.add(Nat.add(p, b), c) == 1n+_ : Nat}
114	      {==}
115	
116	# Four-way regrouping of a sum: (a + b) + (c + d) = (a + c) + (b + d).
117	law add_add_add_comm:
118	  for a: Nat
119	  for b: Nat
120	  for c: Nat
121	  for -d: Nat
122	  {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}
123	
124	def add_add_add_comm(a, b, c, d):
125	  match a:
126	    case 0n:
127	      add_left_comm(b, c, d)
128	    case 1n+p:
129	      %add_add_add_comm(p, b, c, d) : {1n+Nat.add(Nat.add(p, b), Nat.add(c, d)) == 1n+_ : Nat}
130	      {==}
131	
132	def internal_pred(n: Nat) -> Nat:
133	  match n:
134	    case 0n:
135	      0n
136	    case 1n+p:
137	      p
138	
139	# The successor function is injective: a + 1 = b + 1 implies a = b.
140	law succ_inj:
141	  for -a: Nat
142	  for -b: Nat
143	  for e: {1n+a == 1n+b : Nat}
144	  {a == b : Nat}
145	
146	def succ_inj(a, b, e):
147	  %e : {a == internal_pred(_) : Nat}
148	  {==}
149	
150	def internal_zero_ne_succ(-n: Nat, e: {0n == 1n+n : Nat}) -> Empty:
151	  %e : Bool.pick(Type, Nat.is_eq(_, 0n), Unit, Empty)
152	  Unit{}
153	
154	# Zero is not a successor.
155	law zero_ne_succ:
156	  for -n: Nat
157	  {0n != 1n+n : Nat}
158	
159	def zero_ne_succ(n):
160	  e => internal_zero_ne_succ(n, e)
161	
162	def internal_succ_ne_zero(-n: Nat, e: {1n+n == 0n : Nat}) -> Empty:
163	  %e : Bool.pick(Type, Nat.is_eq(_, 0n), Empty, Unit)
164	  Unit{}
165	
166	# A successor is not zero.
167	law succ_ne_zero:
168	  for -n: Nat
169	  {1n+n != 0n : Nat}
170	
171	def succ_ne_zero(n):
172	  e => internal_succ_ne_zero(n, e)
173	
174	# Addition cancels on the left: a + b = a + c implies b = c.
175	law add_left_cancel:
176	  for a: Nat
177	  for -b: Nat
178	  for -c: Nat
179	  for e: {Nat.add(a, b) == Nat.add(a, c) : Nat}
180	  {b == c : Nat}
181	
182	def add_left_cancel(a, b, c, e):
183	  match a:
184	    case 0n:
185	      e
186	    case 1n+p:
187	      add_left_cancel(p, b, c, succ_inj(Nat.add(p, b), Nat.add(p, c), e))
188	
189	# Addition cancels on the right: a + b = c + b implies a = c.
190	law add_right_cancel:
191	  for a: Nat
192	  for b: Nat
193	  for c: Nat
194	  for e: {Nat.add(a, b) == Nat.add(c, b) : Nat}
195	  {a == c : Nat}
196	
197	def add_right_cancel(a, b, c, e):
198	  +b = b
199	  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))))
200	
201	# Zero absorbs multiplication on the right: x * 0 = 0.
202	law mul_zero:
203	  for x: Nat
204	  {Nat.mul(x, 0n) == 0n : Nat}
205	
206	def mul_zero(x):
207	  match x:
208	    case 0n:
209	      {==}
210	    case 1n+p:
211	      mul_zero(p)
212	
213	# Zero absorbs multiplication on the left: 0 * x = 0.
214	law zero_mul:
215	  for -x: Nat
216	  {Nat.mul(0n, x) == 0n : Nat}
217	
218	def zero_mul(x):
219	  {==}
220	
221	# One is a right identity for multiplication: x * 1 = x.
222	law mul_one:
223	  for x: Nat
224	  {Nat.mul(x, 1n) == x : Nat}
225	
226	def mul_one(x):
227	  match x:
228	    case 0n:
229	      {==}
230	    case 1n+p:
231	      %mul_one(p) : {1n+Nat.mul(p, 1n) == 1n+_ : Nat}
232	      {==}
233	
234	# One is a left identity for multiplication: 1 * x = x.
235	law one_mul:
236	  for x: Nat
237	  {Nat.mul(1n, x) == x : Nat}
238	
239	def one_mul(x):
240	  add_zero(x)
241	
242	# Multiplying by a successor on the right: n * (m + 1) = n * m + n.
243	law mul_succ:
244	  for n: Nat
245	  for m: Nat
246	  {Nat.mul(n, 1n+m) == Nat.add(Nat.mul(n, m), n) : Nat}
247	
248	def mul_succ(n, m):
249	  match n:
250	    case 0n:
251	      {==}
252	    case 1n++p:
253	      +m = m
254	      %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}
255	      %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}
256	      %mul_succ(p, m) : {1n+Nat.add(m, Nat.mul(p, 1n+m)) == 1n+Nat.add(m, _) : Nat}
257	      {==}
258	
259	# Multiplying by a successor on the left: (n + 1) * m = n * m + m.
260	law succ_mul:
261	  for n: Nat
262	  for m: Nat
263	  {Nat.mul(1n+n, m) == Nat.add(Nat.mul(n, m), m) : Nat}
264	
265	def succ_mul(n, m):
266	  +m = m
267	  add_comm(m, Nat.mul(n, m))
268	
269	# Multiplication is commutative: n * m = m * n.
270	law mul_comm:
271	  for n: Nat
272	  for m: Nat
273	  {Nat.mul(n, m) == Nat.mul(m, n) : Nat}
274	
275	def mul_comm(n, m):
276	  match n:
277	    case 0n:
278	      %mul_zero(m) : {_ == Nat.mul(m, 0n) : Nat}
279	      {==}
280	    case 1n++p:
281	      +m = m
282	      %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}
283	      %mul_comm(p, m) : {Nat.add(m, Nat.mul(p, m)) == Nat.add(_, m) : Nat}
284	      add_comm(m, Nat.mul(p, m))
285	
286	# Multiplication distributes over addition on the right: (a + b) * c = a * c + b * c.
287	law add_mul:
288	  for a: Nat
289	  for -b: Nat
290	  for c: Nat
291	  {Nat.mul(Nat.add(a, b), c) == Nat.add(Nat.mul(a, c), Nat.mul(b, c)) : Nat}
292	
293	def add_mul(a, b, c):
294	  match a:
295	    case 0n:
296	      {==}
297	    case 1n+p:
298	      +c = c
299	      %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}
300	      %add_mul(p, b, c) : {Nat.add(c, Nat.mul(Nat.add(p, b), c)) == Nat.add(c, _) : Nat}
301	      {==}
302	
303	# Multiplication distributes over addition on the left: a * (b + c) = a * b + a * c.
304	law mul_add:
305	  for a: Nat
306	  for b: Nat
307	  for c: Nat
308	  {Nat.mul(a, Nat.add(b, c)) == Nat.add(Nat.mul(a, b), Nat.mul(a, c)) : Nat}
309	
310	def mul_add(a, b, c):
311	  match a:
312	    case 0n:
313	      {==}
314	    case 1n++p:
315	      +b = b
316	      +c = c
317	      %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}
318	      add_add_add_comm(b, c, Nat.mul(p, b), Nat.mul(p, c))
319	
320	# Multiplication is associative: (a * b) * c = a * (b * c).
321	law mul_assoc:
322	  for a: Nat
323	  for b: Nat
324	  for c: Nat
325	  {Nat.mul(Nat.mul(a, b), c) == Nat.mul(a, Nat.mul(b, c)) : Nat}
326	
327	def mul_assoc(a, b, c):
328	  match a:
329	    case 0n:
330	      {==}
331	    case 1n+p:
332	      +b = b
333	      +c = c
334	      %mul_assoc(p, b, c) : {Nat.mul(Nat.add(b, Nat.mul(p, b)), c) == Nat.add(Nat.mul(b, c), _) : Nat}
335	      add_mul(b, Nat.mul(p, b), c)
336	
337	# The order a <= b on naturals, as a reusable proposition.
338	def le(a: Nat, b: Nat) -> Data:
339	  {Nat.is_le(a, b) == True{} : Bool}
340	
341	# The strict order a < b on naturals, as a reusable proposition.
342	def lt(a: Nat, b: Nat) -> Data:
343	  {Nat.is_lt(a, b) == True{} : Bool}
344	
345	# The order a >= b on naturals, as a reusable proposition.
346	def ge(a: Nat, b: Nat) -> Data:
347	  {Nat.is_ge(a, b) == True{} : Bool}
348	
349	# The strict order a > b on naturals, as a reusable proposition.
350	def gt(a: Nat, b: Nat) -> Data:
351	  {Nat.is_gt(a, b) == True{} : Bool}
352	
353	def internal_false_ne_true(e: {False{} == True{} : Bool}) -> Empty:
354	  %e : Bool.pick(Type, _, Empty, Unit)
355	  Unit{}
356	
357	# Every natural is at most itself: a <= a.
358	law le_refl:
359	  for a: Nat
360	  le(a, a)
361	
362	def le_refl(a):
363	  match a:
364	    case 0n:
365	      {==}
366	    case 1n+p:
367	      le_refl(p)
368	
369	# Zero is at most every natural: 0 <= b.
370	law zero_le:
371	  for b: Nat
372	  le(0n, b)
373	
374	def zero_le(b):
375	  match b:
376	    case 0n:
377	      {==}
378	    case 1n+p:
379	      {==}
380	
381	# Every natural is at most its successor: n <= n + 1.
382	law le_succ:
383	  for n: Nat
384	  le(n, 1n+n)
385	
386	def le_succ(n):
387	  match n:
388	    case 0n:
389	      {==}
390	    case 1n+p:
391	      le_succ(p)
392	
393	# Adding on the right never decreases a natural: n <= n + k.
394	law le_add_right:
395	  for n: Nat
396	  for k: Nat
397	  le(n, Nat.add(n, k))
398	
399	def le_add_right(n, k):
400	  match n:
401	    case 0n:
402	      zero_le(k)
403	    case 1n+p:
404	      le_add_right(p, k)
405	
406	# The order is transitive: a <= b and b <= c imply a <= c.
407	law le_trans:
408	  for a: Nat
409	  for b: Nat
410	  for c: Nat
411	  for ab: le(a, b)
412	  for bc: le(b, c)
413	  le(a, c)
414	
415	def le_trans(a, b, c, ab, bc):
416	  match a b c:
417	    case 0n _ 0n:
418	      {==}
419	    case 0n _ 1n+r:
420	      {==}
421	    case 1n+p 0n _:
422	      Empty.absurd(le(1n+p, c), internal_false_ne_true(ab))
423	    case 1n+p 1n+q 0n:
424	      Empty.absurd(le(1n+p, 0n), internal_false_ne_true(bc))
425	    case 1n+p 1n+q 1n+r:
426	      le_trans(p, q, r, ab, bc)
427	
428	# The order is antisymmetric: a <= b and b <= a imply a = b.
429	law le_antisymm:
430	  for a: Nat
431	  for b: Nat
432	  for ab: le(a, b)
433	  for ba: le(b, a)
434	  {a == b : Nat}
435	
436	def le_antisymm(a, b, ab, ba):
437	  match a b:
438	    case 0n 0n:
439	      {==}
440	    case 0n 1n+q:
441	      Empty.absurd({0n == 1n+q : Nat}, internal_false_ne_true(ba))
442	    case 1n+p 0n:
443	      Empty.absurd({1n+p == 0n : Nat}, internal_false_ne_true(ab))
444	    case 1n+p 1n+q:
445	      %le_antisymm(p, q, ab, ba) : {1n+p == 1n+_ : Nat}
446	      {==}
447	
448	# The order is total: a <= b or b <= a.
449	law le_total:
450	  for a: Nat
451	  for b: Nat
452	  Or(le(a, b), le(b, a))
453	
454	def le_total(a, b):
455	  match a b:
456	    case 0n 0n:
457	      Inl{{==}}
458	    case 0n 1n+q:
459	      Inl{{==}}
460	    case 1n+p 0n:
461	      Inr{{==}}
462	    case 1n+p 1n+q:
463	      le_total(p, q)
464	
465	# The order is total, as a reusable sum: a <= b or b <= a.
466	law le_total_d:
467	  for a: Nat
468	  for b: Nat
469	  Either<&2, &2, le(a, b), le(b, a)>
470	
471	def le_total_d(a, b):
472	  match a b:
473	    case 0n 0n:
474	      Inl{{==}}
475	    case 0n 1n+q:
476	      Inl{{==}}
477	    case 1n+p 0n:
478	      Inr{{==}}
479	    case 1n+p 1n+q:
480	      le_total_d(p, q)
481	
482	# No natural is less than itself.
483	law lt_irrefl:
484	  for a: Nat
485	  lt(a, a) -> Empty
486	
487	def lt_irrefl(a):
488	  match a:
489	    case 0n:
490	      h => internal_false_ne_true(h)
491	    case 1n+p:
492	      lt_irrefl(p)
493	
494	# The strict order is transitive: a < b and b < c imply a < c.
495	law lt_trans:
496	  for a: Nat
497	  for b: Nat
498	  for c: Nat
499	  for ab: lt(a, b)
500	  for bc: lt(b, c)
501	  lt(a, c)
502	
503	def lt_trans(a, b, c, ab, bc):
504	  match a b c:
505	    case 0n 0n _:
506	      Empty.absurd(lt(0n, c), internal_false_ne_true(ab))
507	    case 0n 1n+q 0n:
508	      Empty.absurd(lt(0n, 0n), internal_false_ne_true(bc))
509	    case 0n 1n+q 1n+r:
510	      {==}
511	    case 1n+p 0n _:
512	      Empty.absurd(lt(1n+p, c), internal_false_ne_true(ab))
513	    case 1n+p 1n+q 0n:
514	      Empty.absurd(lt(1n+p, 0n), internal_false_ne_true(bc))
515	    case 1n+p 1n+q 1n+r:
516	      lt_trans(p, q, r, ab, bc)
517	
518	# A strict inequality implies the weak one: a < b implies a <= b.
519	law le_of_lt:
520	  for a: Nat
521	  for b: Nat
522	  for h: lt(a, b)
523	  le(a, b)
524	
525	def le_of_lt(a, b, h):
526	  match a b:
527	    case 0n 0n:
528	      {==}
529	    case 0n 1n+q:
530	      {==}
531	    case 1n+p 0n:
532	      Empty.absurd(le(1n+p, 0n), internal_false_ne_true(h))
533	    case 1n+p 1n+q:
534	      le_of_lt(p, q, h)
535	
536	# Flipping a >= b gives b <= a.
537	law le_of_ge:
538	  for a: Nat
539	  for b: Nat
540	  for h: ge(a, b)
541	  le(b, a)
542	
543	def le_of_ge(a, b, h):
544	  match a b:
545	    case 0n 0n:
546	      {==}
547	    case 0n 1n+q:
548	      Empty.absurd(le(1n+q, 0n), internal_false_ne_true(h))
549	    case 1n+p 0n:
550	      {==}
551	    case 1n+p 1n+q:
552	      le_of_ge(p, q, h)
553	
554	# Flipping b <= a gives a >= b.
555	law ge_of_le:
556	  for a: Nat
557	  for b: Nat
558	  for h: le(b, a)
559	  ge(a, b)
560	
561	def ge_of_le(a, b, h):
562	  match a b:
563	    case 0n 0n:
564	      {==}
565	    case 0n 1n+q:
566	      Empty.absurd(ge(0n, 1n+q), internal_false_ne_true(h))
567	    case 1n+p 0n:
568	      {==}
569	    case 1n+p 1n+q:
570	      ge_of_le(p, q, h)
571	
572	# Flipping a > b gives b < a.
573	law lt_of_gt:
574	  for a: Nat
575	  for b: Nat
576	  for h: gt(a, b)
577	  lt(b, a)
578	
579	def lt_of_gt(a, b, h):
580	  match a b:
581	    case 0n 0n:
582	      Empty.absurd(lt(0n, 0n), internal_false_ne_true(h))
583	    case 0n 1n+q:
584	      Empty.absurd(lt(1n+q, 0n), internal_false_ne_true(h))
585	    case 1n+p 0n:
586	      {==}
587	    case 1n+p 1n+q:
588	      lt_of_gt(p, q, h)
589	
590	# Flipping b < a gives a > b.
591	law gt_of_lt:
592	  for a: Nat
593	  for b: Nat
594	  for h: lt(b, a)
595	  gt(a, b)
596	
597	def gt_of_lt(a, b, h):
598	  match a b:
599	    case 0n 0n:
600	      Empty.absurd(gt(0n, 0n), internal_false_ne_true(h))
601	    case 0n 1n+q:
602	      Empty.absurd(gt(0n, 1n+q), internal_false_ne_true(h))
603	    case 1n+p 0n:
604	      {==}
605	    case 1n+p 1n+q:
606	      gt_of_lt(p, q, h)
607	
608	# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
609	
610	# Zero is a right identity for addition: x + 0 = x, reversed to rewrite toward the simple side.
611	law add_zero_sym:
612	  for x: Nat
613	  {x == Nat.add(x, 0n) : Nat}
614	
615	def add_zero_sym(x):
616	  Equal.sym(Nat, Nat.add(x, 0n), x, add_zero(x))
617	
618	# Zero is a left identity for addition: 0 + x = x, reversed to rewrite toward the simple side.
619	law zero_add_sym:
620	  for -x: Nat
621	  {x == Nat.add(0n, x) : Nat}
622	
623	def zero_add_sym(x):
624	  Equal.sym(Nat, Nat.add(0n, x), x, zero_add(x))
625	
626	# Adding a successor on the right: n + (m + 1) = (n + m) + 1, reversed to rewrite toward the simple side.
627	law add_succ_sym:
628	  for n: Nat
629	  for -m: Nat
630	  {1n+Nat.add(n, m) == Nat.add(n, 1n+m) : Nat}
631	
632	def add_succ_sym(n, m):
633	  Equal.sym(Nat, Nat.add(n, 1n+m), 1n+Nat.add(n, m), add_succ(n, m))
634	
635	# Adding a successor on the left: (n + 1) + m = (n + m) + 1, reversed to rewrite toward the simple side.
636	law succ_add_sym:
637	  for -n: Nat
638	  for -m: Nat
639	  {1n+Nat.add(n, m) == Nat.add(1n+n, m) : Nat}
640	
641	def succ_add_sym(n, m):
642	  Equal.sym(Nat, Nat.add(1n+n, m), 1n+Nat.add(n, m), succ_add(n, m))
643	
644	# Addition is commutative: n + m = m + n, reversed to rewrite toward the simple side.
645	law add_comm_sym:
646	  for n: Nat
647	  for m: Nat
648	  {Nat.add(m, n) == Nat.add(n, m) : Nat}
649	
650	def add_comm_sym(n, m):
651	  Equal.sym(Nat, Nat.add(n, m), Nat.add(m, n), add_comm(n, m))
652	
653	# Addition is associative: (a + b) + c = a + (b + c), reversed to rewrite toward the simple side.
654	law add_assoc_sym:
655	  for a: Nat
656	  for -b: Nat
657	  for -c: Nat
658	  {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, b), c) : Nat}
659	
660	def add_assoc_sym(a, b, c):
661	  Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(a, Nat.add(b, c)), add_assoc(a, b, c))
662	
663	# Left commutativity of addition: a + (b + c) = b + (a + c), reversed to rewrite toward the simple side.
664	law add_left_comm_sym:
665	  for a: Nat
666	  for b: Nat
667	  for -c: Nat
668	  {Nat.add(b, Nat.add(a, c)) == Nat.add(a, Nat.add(b, c)) : Nat}
669	
670	def add_left_comm_sym(a, b, c):
671	  Equal.sym(Nat, Nat.add(a, Nat.add(b, c)), Nat.add(b, Nat.add(a, c)), add_left_comm(a, b, c))
672	
673	# Right commutativity of addition: (a + b) + c = (a + c) + b, reversed to rewrite toward the simple side.
674	law add_right_comm_sym:
675	  for a: Nat
676	  for b: Nat
677	  for c: Nat
678	  {Nat.add(Nat.add(a, c), b) == Nat.add(Nat.add(a, b), c) : Nat}
679	
680	def add_right_comm_sym(a, b, c):
681	  Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(Nat.add(a, c), b), add_right_comm(a, b, c))
682	
683	# Four-way regrouping of a sum: (a + b) + (c + d) = (a + c) + (b + d), reversed to rewrite toward the simple side.
684	law add_add_add_comm_sym:
685	  for a: Nat
686	  for b: Nat
687	  for c: Nat
688	  for -d: Nat
689	  {Nat.add(Nat.add(a, c), Nat.add(b, d)) == Nat.add(Nat.add(a, b), Nat.add(c, d)) : Nat}
690	
691	def add_add_add_comm_sym(a, b, c, d):
692	  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))
693	
694	# Zero absorbs multiplication on the right: x * 0 = 0, reversed to rewrite toward the simple side.
695	law mul_zero_sym:
696	  for x: Nat
697	  {0n == Nat.mul(x, 0n) : Nat}
698	
699	def mul_zero_sym(x):
700	  Equal.sym(Nat, Nat.mul(x, 0n), 0n, mul_zero(x))
701	
702	# Zero absorbs multiplication on the left: 0 * x = 0, reversed to rewrite toward the simple side.
703	law zero_mul_sym:
704	  for -x: Nat
705	  {0n == Nat.mul(0n, x) : Nat}
706	
707	def zero_mul_sym(x):
708	  Equal.sym(Nat, Nat.mul(0n, x), 0n, zero_mul(x))
709	
710	# One is a right identity for multiplication: x * 1 = x, reversed to rewrite toward the simple side.
711	law mul_one_sym:
712	  for x: Nat
713	  {x == Nat.mul(x, 1n) : Nat}
714	
715	def mul_one_sym(x):
716	  Equal.sym(Nat, Nat.mul(x, 1n), x, mul_one(x))
717	
718	# One is a left identity for multiplication: 1 * x = x, reversed to rewrite toward the simple side.
719	law one_mul_sym:
720	  for x: Nat
721	  {x == Nat.mul(1n, x) : Nat}
722	
723	def one_mul_sym(x):
724	  Equal.sym(Nat, Nat.mul(1n, x), x, one_mul(x))
725	
726	# Multiplying by a successor on the right: n * (m + 1) = n * m + n, reversed to rewrite toward the simple side.
727	law mul_succ_sym:
728	  for n: Nat
729	  for m: Nat
730	  {Nat.add(Nat.mul(n, m), n) == Nat.mul(n, 1n+m) : Nat}
731	
732	def mul_succ_sym(n, m):
733	  Equal.sym(Nat, Nat.mul(n, 1n+m), Nat.add(Nat.mul(n, m), n), mul_succ(n, m))
734	
735	# Multiplying by a successor on the left: (n + 1) * m = n * m + m, reversed to rewrite toward the simple side.
736	law succ_mul_sym:
737	  for n: Nat
738	  for m: Nat
739	  {Nat.add(Nat.mul(n, m), m) == Nat.mul(1n+n, m) : Nat}
740	
741	def succ_mul_sym(n, m):
742	  Equal.sym(Nat, Nat.mul(1n+n, m), Nat.add(Nat.mul(n, m), m), succ_mul(n, m))
743	
744	# Multiplication is commutative: n * m = m * n, reversed to rewrite toward the simple side.
745	law mul_comm_sym:
746	  for n: Nat
747	  for m: Nat
748	  {Nat.mul(m, n) == Nat.mul(n, m) : Nat}
749	
750	def mul_comm_sym(n, m):
751	  Equal.sym(Nat, Nat.mul(n, m), Nat.mul(m, n), mul_comm(n, m))
752	
753	# Multiplication distributes over addition on the right: (a + b) * c = a * c + b * c, reversed to rewrite toward the simple side.
754	law add_mul_sym:
755	  for a: Nat
756	  for -b: Nat
757	  for c: Nat
758	  {Nat.add(Nat.mul(a, c), Nat.mul(b, c)) == Nat.mul(Nat.add(a, b), c) : Nat}
759	
760	def add_mul_sym(a, b, c):
761	  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))
762	
763	# Multiplication distributes over addition on the left: a * (b + c) = a * b + a * c, reversed to rewrite toward the simple side.
764	law mul_add_sym:
765	  for a: Nat
766	  for b: Nat
767	  for c: Nat
768	  {Nat.add(Nat.mul(a, b), Nat.mul(a, c)) == Nat.mul(a, Nat.add(b, c)) : Nat}
769	
770	def mul_add_sym(a, b, c):
771	  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))
772	
773	# Multiplication is associative: (a * b) * c = a * (b * c), reversed to rewrite toward the simple side.
774	law mul_assoc_sym:
775	  for a: Nat
776	  for b: Nat
777	  for c: Nat
778	  {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(Nat.mul(a, b), c) : Nat}
779	
780	def mul_assoc_sym(a, b, c):
781	  Equal.sym(Nat, Nat.mul(Nat.mul(a, b), c), Nat.mul(a, Nat.mul(b, c)), mul_assoc(a, b, c))