nat.bend

bend-mathlib@0.6.0.0 · 3,284 lines · 0 definitions

1# bend-mathlib/nat.bend: Nat arithmetic (add, mul, sub, min, max, pow) and order (le, lt, ge, gt).
2import Base
3
4# Zero is a right identity for addition: x + 0 = x.
5law add_zero:
6  for x: Nat
7  {Nat.add(x, 0n) == x : Nat}
8
9def 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.
18law zero_add:
19  for -x: Nat
20  {Nat.add(0n, x) == x : Nat}
21
22def zero_add(x):
23  {==}
24
25# Adding a successor on the right: n + (m + 1) = (n + m) + 1.
26law add_succ:
27  for n: Nat
28  for -m: Nat
29  {Nat.add(n, 1n+m) == 1n+Nat.add(n, m) : Nat}
30
31def 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.
40law succ_add:
41  for -n: Nat
42  for -m: Nat
43  {Nat.add(1n+n, m) == 1n+Nat.add(n, m) : Nat}
44
45def succ_add(n, m):
46  {==}
47
48# Addition is commutative: n + m = m + n.
49law add_comm:
50  for n: Nat
51  for m: Nat
52  {Nat.add(n, m) == Nat.add(m, n) : Nat}
53
54def 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).
71law 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
77def 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).
86law 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
92def 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.
103law 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
109def 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).
118law 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
125def 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
133def 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.
141law succ_inj:
142  for -a: Nat
143  for -b: Nat
144  for e: {1n+a == 1n+b : Nat}
145  {a == b : Nat}
146
147def succ_inj(a, b, e):
148  %e : {a == internal_pred(_) : Nat}
149  {==}
150
151def 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.
156law zero_ne_succ:
157  for -n: Nat
158  {0n != 1n+n : Nat}
159
160def zero_ne_succ(n):
161  e => internal_zero_ne_succ(n, e)
162
163def 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.
168law succ_ne_zero:
169  for -n: Nat
170  {1n+n != 0n : Nat}
171
172def 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.
176law 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
183def 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.
191law 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
198def 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.
203law mul_zero:
204  for x: Nat
205  {Nat.mul(x, 0n) == 0n : Nat}
206
207def 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.
215law zero_mul:
216  for -x: Nat
217  {Nat.mul(0n, x) == 0n : Nat}
218
219def zero_mul(x):
220  {==}
221
222# One is a right identity for multiplication: x * 1 = x.
223law mul_one:
224  for x: Nat
225  {Nat.mul(x, 1n) == x : Nat}
226
227def 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.
236law one_mul:
237  for x: Nat
238  {Nat.mul(1n, x) == x : Nat}
239
240def one_mul(x):
241  add_zero(x)
242
243# Multiplying by a successor on the right: n * (m + 1) = n * m + n.
244law 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
249def 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.
261law 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
266def succ_mul(n, m):
267  +m = m
268  add_comm(m, Nat.mul(n, m))
269
270# Multiplication is commutative: n * m = m * n.
271law mul_comm:
272  for n: Nat
273  for m: Nat
274  {Nat.mul(n, m) == Nat.mul(m, n) : Nat}
275
276def 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.
288law 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
294def 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.
305law 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
311def 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).
322law 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
328def 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.
339def 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.
343def 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.
347def 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.
351def gt(a: Nat, b: Nat) -> Data:
352  {Nat.is_gt(a, b) == True{} : Bool}
353
354def 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.
359law le_refl:
360  for a: Nat
361  le(a, a)
362
363def 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.
371law zero_le:
372  for b: Nat
373  le(0n, b)
374
375def 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.
383law le_succ:
384  for n: Nat
385  le(n, 1n+n)
386
387def 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.
395law le_add_right:
396  for n: Nat
397  for k: Nat
398  le(n, Nat.add(n, k))
399
400def 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.
408law 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
416def 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.
430law 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
437def 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.
450law le_total:
451  for a: Nat
452  for b: Nat
453  Or(le(a, b), le(b, a))
454
455def 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.
467law le_total_d:
468  for a: Nat
469  for b: Nat
470  Either<&2, &2, le(a, b), le(b, a)>
471
472def 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.
484law lt_irrefl:
485  for a: Nat
486  lt(a, a) -> Empty
487
488def 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.
496law 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
504def 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.
520law le_of_lt:
521  for a: Nat
522  for b: Nat
523  for h: lt(a, b)
524  le(a, b)
525
526def 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.
538law le_of_ge:
539  for a: Nat
540  for b: Nat
541  for h: ge(a, b)
542  le(b, a)
543
544def 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.
556law ge_of_le:
557  for a: Nat
558  for b: Nat
559  for h: le(b, a)
560  ge(a, b)
561
562def 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.
574law lt_of_gt:
575  for a: Nat
576  for b: Nat
577  for h: gt(a, b)
578  lt(b, a)
579
580def 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.
592law gt_of_lt:
593  for a: Nat
594  for b: Nat
595  for h: lt(b, a)
596  gt(a, b)
597
598def 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.
610law sub_zero:
611  for n: Nat
612  {Nat.sub(n, 0n) == n : Nat}
613
614def 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.
622law zero_sub:
623  for n: Nat
624  {Nat.sub(0n, n) == 0n : Nat}
625
626def 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.
634law sub_self:
635  for n: Nat
636  {Nat.sub(n, n) == 0n : Nat}
637
638def 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.
646law succ_sub_succ:
647  for -n: Nat
648  for -m: Nat
649  {Nat.sub(1n+n, 1n+m) == Nat.sub(n, m) : Nat}
650
651def succ_sub_succ(n, m):
652  {==}
653
654# Adding then subtracting m cancels: (n + m) - m = n.
655law add_sub_cancel:
656  for n: Nat
657  for m: Nat
658  {Nat.sub(Nat.add(n, m), m) == n : Nat}
659
660def 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.
672law add_sub_cancel_left:
673  for n: Nat
674  for m: Nat
675  {Nat.sub(Nat.add(n, m), n) == m : Nat}
676
677def 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.
685law 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
691def 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).
706law 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
712def 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.
724law sub_le:
725  for n: Nat
726  for m: Nat
727  le(Nat.sub(n, m), n)
728
729def 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
740def internal_div_true_ne_false(h: {True{} == False{} : Bool}) -> Empty:
741  internal_false_ne_true(Equal.sym(Bool, True{}, False{}, h))
742
743def 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
746def 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
749def 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
752def 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
756def 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
760def 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.
776law 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
781def 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
785def 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
790def 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
799def 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
806def 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.
813law 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
819def div_eq_zero_of_le(a, b, h):
820  internal_div_zero_of_wit(a, b, internal_div_le_wit(a, b, h))
821
822def 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
831def 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
840def 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
849def 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).
856law 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
863def div_le_div(a, c, b, h):
864  internal_div_mono_wit(a, c, b, internal_div_le_wit(a, c, h))
865
866def 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
875def 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).
884law 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
889def 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
894def 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
901def 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
908def 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
917def 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
925def 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
933def 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.
941law 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
947def 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.
957law min_comm:
958  for a: Nat
959  for b: Nat
960  {Nat.min(a, b) == Nat.min(b, a) : Nat}
961
962def 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.
975law max_comm:
976  for a: Nat
977  for b: Nat
978  {Nat.max(a, b) == Nat.max(b, a) : Nat}
979
980def 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.
993law min_self:
994  for a: Nat
995  {Nat.min(a, a) == a : Nat}
996
997def 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.
1006law max_self:
1007  for a: Nat
1008  {Nat.max(a, a) == a : Nat}
1009
1010def 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.
1019law min_zero:
1020  for a: Nat
1021  {Nat.min(a, 0n) == 0n : Nat}
1022
1023def 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.
1031law zero_min:
1032  for a: Nat
1033  {Nat.min(0n, a) == 0n : Nat}
1034
1035def 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.
1043law max_zero:
1044  for a: Nat
1045  {Nat.max(a, 0n) == a : Nat}
1046
1047def 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.
1055law zero_max:
1056  for a: Nat
1057  {Nat.max(0n, a) == a : Nat}
1058
1059def zero_max(a):
1060  match a:
1061    case 0n:
1062      {==}
1063    case 1n+p:
1064      {==}
1065
1066# Minimum is associative.
1067law 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
1073def 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.
1086law 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
1092def 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.
1105law 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
1110def 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.
1126law min_le_left:
1127  for a: Nat
1128  for b: Nat
1129  le(Nat.min(a, b), a)
1130
1131def 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.
1143law min_le_right:
1144  for a: Nat
1145  for b: Nat
1146  le(Nat.min(a, b), b)
1147
1148def 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.
1160law le_max_left:
1161  for a: Nat
1162  for b: Nat
1163  le(a, Nat.max(a, b))
1164
1165def 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.
1177law le_max_right:
1178  for a: Nat
1179  for b: Nat
1180  le(b, Nat.max(a, b))
1181
1182def 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.
1194law pow_zero:
1195  for -a: Nat
1196  {Nat.pow(a, 0n) == 1n : Nat}
1197
1198def pow_zero(a):
1199  {==}
1200
1201# A power with a successor exponent: a^(n+1) = a * a^n.
1202law 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
1207def pow_succ(a, n):
1208  {==}
1209
1210# Any natural to the power one is itself.
1211law pow_one:
1212  for a: Nat
1213  {Nat.pow(a, 1n) == a : Nat}
1214
1215def pow_one(a):
1216  mul_one(a)
1217
1218# One to any power is one.
1219law one_pow:
1220  for n: Nat
1221  {Nat.pow(1n, n) == 1n : Nat}
1222
1223def 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.
1232law 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
1238def 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.
1252law double_eq_add:
1253  for n: Nat
1254  {Nat.double(n) == Nat.add(n, n) : Nat}
1255
1256def 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.
1266law is_eq_refl:
1267  for n: Nat
1268  {Nat.is_eq(n, n) == True{} : Bool}
1269
1270def 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.
1278law is_eq_comm:
1279  for a: Nat
1280  for b: Nat
1281  {Nat.is_eq(a, b) == Nat.is_eq(b, a) : Bool}
1282
1283def 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.
1296law 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
1302def 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.
1315law 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
1320def 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.
1333law 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
1338def 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.
1351law 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
1356def 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.
1372law 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
1377def 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.
1389law 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
1394def 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.
1406law lt_succ_self:
1407  for n: Nat
1408  lt(n, 1n+n)
1409
1410def 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.
1418law succ_le_succ:
1419  for -a: Nat
1420  for -b: Nat
1421  for h: le(a, b)
1422  le(1n+a, 1n+b)
1423
1424def 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.
1428law 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
1434def le_of_succ_le_succ(a, b, h):
1435  h
1436
1437# A < b and b <= c imply a < c.
1438law 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
1446def 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.
1462law 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
1470def 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.
1486law 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
1493def 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.
1501law 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
1508def 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.
1514law 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
1520def 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.
1528law 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
1537def 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.
1541law 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
1547def 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.
1559law le_zero_eq:
1560  for n: Nat
1561  for h: le(n, 0n)
1562  {n == 0n : Nat}
1563
1564def 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.
1572law lt_zero:
1573  for n: Nat
1574  lt(n, 0n) -> Empty
1575
1576def 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.
1584law 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
1590def 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.
1602law 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
1608def 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.
1620law 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
1626def 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.
1638law 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
1644def 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.
1656law 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
1664def 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
1675def internal_or_true_sym(x: Bool) -> {True{} == Bool.or(x, True{}) : Bool}:
1676  match x:
1677    case False{}:
1678      {==}
1679    case True{}:
1680      {==}
1681
1682def 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.
1690law 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
1696def 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.
1716law 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
1722def 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.
1742law 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
1748def 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.
1760law 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
1766def 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.
1778law 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
1784def 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
1796def 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.
1804law 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
1810def 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.
1822law 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
1829def 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.
1834law 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
1841def 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.
1848law zero_div:
1849  for b: Nat
1850  {Nat.div(0n, b) == 0n : Nat}
1851
1852def 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.
1860law zero_mod:
1861  for b: Nat
1862  {Nat.mod(0n, b) == 0n : Nat}
1863
1864def zero_mod(b):
1865  match b:
1866    case 0n:
1867      {==}
1868    case 1n+p:
1869      {==}
1870
1871def 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.
1880law div_one:
1881  for a: Nat
1882  {Nat.div(a, 1n) == a : Nat}
1883
1884def 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.
1890law mod_one:
1891  for a: Nat
1892  {Nat.mod(a, 1n) == 0n : Nat}
1893
1894def mod_one(a):
1895  +a = a
1896  %internal_div_go_one(a, 0n) : {Pair.snd(Nat, Nat, _) == 0n : Nat}
1897  {==}
1898
1899def 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.
1907law mod_self:
1908  for n: Nat
1909  {Nat.mod(n, n) == 0n : Nat}
1910
1911def 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.
1920law div_self:
1921  for b: Nat
1922  {Nat.div(1n+b, 1n+b) == 1n : Nat}
1923
1924def div_self(b):
1925  +b = b
1926  %internal_div_go_self(b, 0n, 0n) : {Pair.fst(Nat, Nat, _) == 1n : Nat}
1927  {==}
1928
1929def 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.
1941law mod_lt:
1942  for a: Nat
1943  for b: Nat
1944  lt(Nat.mod(a, 1n+b), 1n+b)
1945
1946def 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.
1953law mod_le:
1954  for a: Nat
1955  for b: Nat
1956  le(Nat.mod(a, b), a)
1957
1958def 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
1967def 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.
1973law div_le_self:
1974  for a: Nat
1975  for b: Nat
1976  le(Nat.div(a, b), a)
1977
1978def 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
1987def 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
1995def 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
2001# A number below the divisor is its own remainder: a < b implies a % b = a.
2002law mod_eq_of_lt:
2003  for a: Nat
2004  for b: Nat
2005  for h: lt(a, b)
2006  {Nat.mod(a, b) == a : Nat}
2007
2008def mod_eq_of_lt(a, b, h):
2009  match b:
2010    case 0n:
2011      +a = a
2012      Empty.absurd({Nat.mod(a, 0n) == a : Nat}, lt_zero(a)(h))
2013    case 1n++bp:
2014      +a = a
2015      +bp = bp
2016      internal_mod_eq_of_wit(a, bp, internal_div_le_wit(a, bp, Equal.trans(Bool, Nat.is_le(1n+a, 1n+bp), Nat.is_lt(a, 1n+bp), True{}, Equal.sym(Bool, Nat.is_lt(a, 1n+bp), Nat.is_le(1n+a, 1n+bp), is_lt_eq_succ_le(a, 1n+bp)), h)))
2017
2018# Taking a remainder twice is taking it once: (a % n) % n = a % n.
2019law mod_mod:
2020  for a: Nat
2021  for n: Nat
2022  {Nat.mod(Nat.mod(a, n), n) == Nat.mod(a, n) : Nat}
2023
2024def mod_mod(a, n):
2025  match n:
2026    case 0n:
2027      {==}
2028    case 1n++b:
2029      +a = a
2030      +b = b
2031      mod_eq_of_lt(Nat.mod(a, 1n+b), 1n+b, mod_lt(a, b))
2032
2033def internal_mod_go_d(n: Nat, m: Nat, -d: Nat, -e: Nat, r: Nat) -> {Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d, r)) == Pair.snd(Nat, Nat, Nat.divmod.go(n, m, e, r)) : Nat}:
2034  match n m:
2035    case 0n _:
2036      {==}
2037    case 1n+np 0n:
2038      internal_mod_go_d(np, r, 1n+d, 1n+e, 0n)
2039    case 1n+np 1n+mp:
2040      internal_mod_go_d(np, mp, d, e, 1n+r)
2041
2042# Adding the divisor does not change the remainder: (b + a) % b = a % b.
2043law add_mod_left:
2044  for a: Nat
2045  for b: Nat
2046  {Nat.mod(Nat.add(b, a), b) == Nat.mod(a, b) : Nat}
2047
2048def add_mod_left(a, b):
2049  match b:
2050    case 0n:
2051      {==}
2052    case 1n++bp:
2053      +a = a
2054      %internal_div_go_run(bp, a, 0n, 0n) : {Pair.snd(Nat, Nat, _) == Nat.mod(a, 1n+bp) : Nat}
2055      %internal_div_add_zero_r(bp) : {Pair.snd(Nat, Nat, Nat.divmod.go(a, _, 1n, 0n)) == Nat.mod(a, 1n+bp) : Nat}
2056      internal_mod_go_d(a, bp, 1n, 0n, 0n)
2057
2058# Multiplying by a positive divisor then dividing by it cancels: (a * (1 + b)) / (1 + b) = a.
2059law mul_div_cancel:
2060  for a: Nat
2061  for b: Nat
2062  {Nat.div(Nat.mul(a, 1n+b), 1n+b) == a : Nat}
2063
2064def mul_div_cancel(a, b):
2065  match a:
2066    case 0n:
2067      {==}
2068    case 1n++p:
2069      +b = b
2070      %Equal.sym(Nat, Nat.div(Nat.add(1n+b, Nat.mul(p, 1n+b)), 1n+b), 1n+Nat.div(Nat.mul(p, 1n+b), 1n+b), add_div_left(Nat.mul(p, 1n+b), b)) : {_ == 1n+p : Nat}
2071      %mul_div_cancel(p, b) : {1n+Nat.div(Nat.mul(p, 1n+b), 1n+b) == 1n+_ : Nat}
2072      {==}
2073
2074# Multiplying on the left by a positive divisor then dividing by it cancels: ((1 + b) * a) / (1 + b) = a.
2075law mul_div_cancel_left:
2076  for a: Nat
2077  for b: Nat
2078  {Nat.div(Nat.mul(1n+b, a), 1n+b) == a : Nat}
2079
2080def mul_div_cancel_left(a, b):
2081  +a = a
2082  +b = b
2083  %mul_comm(a, 1n+b) : {Nat.div(_, 1n+b) == a : Nat}
2084  mul_div_cancel(a, b)
2085
2086# A multiple of b leaves no remainder modulo b: (a * b) % b = 0.
2087law mul_mod_left:
2088  for a: Nat
2089  for b: Nat
2090  {Nat.mod(Nat.mul(a, b), b) == 0n : Nat}
2091
2092def mul_mod_left(a, b):
2093  match a b:
2094    case _ 0n:
2095      mul_zero(a)
2096    case 0n 1n+bp:
2097      {==}
2098    case 1n++p 1n++bp:
2099      Equal.trans(Nat, Nat.mod(Nat.add(1n+bp, Nat.mul(p, 1n+bp)), 1n+bp), Nat.mod(Nat.mul(p, 1n+bp), 1n+bp), 0n, add_mod_left(Nat.mul(p, 1n+bp), 1n+bp), mul_mod_left(p, 1n+bp))
2100
2101# A multiple of a leaves no remainder modulo a: (a * b) % a = 0.
2102law mul_mod_right:
2103  for a: Nat
2104  for b: Nat
2105  {Nat.mod(Nat.mul(a, b), a) == 0n : Nat}
2106
2107def mul_mod_right(a, b):
2108  +a = a
2109  +b = b
2110  %mul_comm(b, a) : {Nat.mod(_, a) == 0n : Nat}
2111  mul_mod_left(b, a)
2112
2113# The remainder plus the divisor times the quotient is the dividend: a % b + b * (a / b) = a.
2114law mod_add_div:
2115  for a: Nat
2116  for b: Nat
2117  {Nat.add(Nat.mod(a, b), Nat.mul(b, Nat.div(a, b))) == a : Nat}
2118
2119def mod_add_div(a, b):
2120  match b:
2121    case 0n:
2122      add_zero(a)
2123    case 1n++bp:
2124      +a = a
2125      %add_comm(Nat.mul(1n+bp, Nat.div(a, 1n+bp)), Nat.mod(a, 1n+bp)) : {_ == a : Nat}
2126      %mul_comm(Nat.div(a, 1n+bp), 1n+bp) : {Nat.add(_, Nat.mod(a, 1n+bp)) == a : Nat}
2127      div_mod_eq(a, bp)
2128
2129# The quotient times the divisor never exceeds the dividend: (a / b) * b <= a.
2130law div_mul_le_self:
2131  for a: Nat
2132  for b: Nat
2133  le(Nat.mul(Nat.div(a, b), b), a)
2134
2135def div_mul_le_self(a, b):
2136  match b:
2137    case 0n:
2138      zero_le(a)
2139    case 1n++bp:
2140      +a = a
2141      le_of_add_eq(Nat.mul(Nat.div(a, 1n+bp), 1n+bp), Nat.mod(a, 1n+bp), a, div_mod_eq(a, bp))
2142
2143# Left commutativity of multiplication: a * (b * c) = b * (a * c).
2144law mul_left_comm:
2145  for a: Nat
2146  for b: Nat
2147  for c: Nat
2148  {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(b, Nat.mul(a, c)) : Nat}
2149
2150def mul_left_comm(a, b, c):
2151  +a = a
2152  +b = b
2153  +c = c
2154  %mul_assoc(a, b, c) : {_ == Nat.mul(b, Nat.mul(a, c)) : Nat}
2155  %mul_comm(b, a) : {Nat.mul(_, c) == Nat.mul(b, Nat.mul(a, c)) : Nat}
2156  mul_assoc(b, a, c)
2157
2158# Right commutativity of multiplication: (a * b) * c = (a * c) * b.
2159law mul_right_comm:
2160  for a: Nat
2161  for b: Nat
2162  for c: Nat
2163  {Nat.mul(Nat.mul(a, b), c) == Nat.mul(Nat.mul(a, c), b) : Nat}
2164
2165def mul_right_comm(a, b, c):
2166  +a = a
2167  +b = b
2168  +c = c
2169  %Equal.sym(Nat, Nat.mul(Nat.mul(a, c), b), Nat.mul(a, Nat.mul(c, b)), mul_assoc(a, c, b)) : {Nat.mul(Nat.mul(a, b), c) == _ : Nat}
2170  %mul_comm(b, c) : {Nat.mul(Nat.mul(a, b), c) == Nat.mul(a, _) : Nat}
2171  mul_assoc(a, b, c)
2172
2173# Four-way regrouping of a product: (a * b) * (c * d) = (a * c) * (b * d).
2174law mul_mul_mul_comm:
2175  for a: Nat
2176  for b: Nat
2177  for c: Nat
2178  for d: Nat
2179  {Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) == Nat.mul(Nat.mul(a, c), Nat.mul(b, d)) : Nat}
2180
2181def mul_mul_mul_comm(a, b, c, d):
2182  +a = a
2183  +b = b
2184  +c = c
2185  +d = d
2186  %Equal.sym(Nat, Nat.mul(Nat.mul(a, c), Nat.mul(b, d)), Nat.mul(a, Nat.mul(c, Nat.mul(b, d))), mul_assoc(a, c, Nat.mul(b, d))) : {Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) == _ : Nat}
2187  %mul_left_comm(b, c, d) : {Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) == Nat.mul(a, _) : Nat}
2188  mul_assoc(a, b, Nat.mul(c, d))
2189
2190# Zero to a positive power is zero: 0^(n+1) = 0.
2191law zero_pow:
2192  for -n: Nat
2193  {Nat.pow(0n, 1n+n) == 0n : Nat}
2194
2195def zero_pow(n):
2196  {==}
2197
2198# A power of a product is the product of the powers: (a * b)^n = a^n * b^n.
2199law mul_pow:
2200  for +a: Nat
2201  for +b: Nat
2202  for n: Nat
2203  {Nat.pow(Nat.mul(a, b), n) == Nat.mul(Nat.pow(a, n), Nat.pow(b, n)) : Nat}
2204
2205def mul_pow(a, b, n):
2206  match n:
2207    case 0n:
2208      {==}
2209    case 1n++p:
2210      %Equal.sym(Nat, Nat.pow(Nat.mul(a, b), p), Nat.mul(Nat.pow(a, p), Nat.pow(b, p)), mul_pow(a, b, p)) : {Nat.mul(Nat.mul(a, b), _) == Nat.mul(Nat.mul(a, Nat.pow(a, p)), Nat.mul(b, Nat.pow(b, p))) : Nat}
2211      mul_mul_mul_comm(a, b, Nat.pow(a, p), Nat.pow(b, p))
2212
2213# Exponents multiply under repeated powers: a^(m * n) = (a^m)^n.
2214law pow_mul:
2215  for a: Nat
2216  for m: Nat
2217  for n: Nat
2218  {Nat.pow(a, Nat.mul(m, n)) == Nat.pow(Nat.pow(a, m), n) : Nat}
2219
2220def pow_mul(a, m, n):
2221  match m:
2222    case 0n:
2223      Equal.sym(Nat, Nat.pow(1n, n), 1n, one_pow(n))
2224    case 1n++p:
2225      +a = a
2226      +n = n
2227      %Equal.sym(Nat, Nat.pow(Nat.mul(a, Nat.pow(a, p)), n), Nat.mul(Nat.pow(a, n), Nat.pow(Nat.pow(a, p), n)), mul_pow(a, Nat.pow(a, p), n)) : {Nat.pow(a, Nat.add(n, Nat.mul(p, n))) == _ : Nat}
2228      %pow_mul(a, p, n) : {Nat.pow(a, Nat.add(n, Nat.mul(p, n))) == Nat.mul(Nat.pow(a, n), _) : Nat}
2229      pow_add(a, n, Nat.mul(p, n))
2230
2231# A power of a positive base is at least one: 1 <= (1 + a)^n.
2232law one_le_pow:
2233  for n: Nat
2234  for a: Nat
2235  le(1n, Nat.pow(1n+a, n))
2236
2237def one_le_pow(n, a):
2238  match n:
2239    case 0n:
2240      {==}
2241    case 1n++p:
2242      +a = a
2243      le_trans(1n, Nat.pow(1n+a, p), Nat.add(Nat.pow(1n+a, p), Nat.mul(a, Nat.pow(1n+a, p))), one_le_pow(p, a), le_add_right(Nat.pow(1n+a, p), Nat.mul(a, Nat.pow(1n+a, p))))
2244
2245# A power of a positive base is positive: 0 < (1 + a)^n.
2246law pow_pos:
2247  for n: Nat
2248  for a: Nat
2249  lt(0n, Nat.pow(1n+a, n))
2250
2251def pow_pos(n, a):
2252  +n = n
2253  +a = a
2254  %Equal.sym(Bool, Nat.is_lt(0n, Nat.pow(1n+a, n)), Nat.is_le(1n, Nat.pow(1n+a, n)), is_lt_eq_succ_le(0n, Nat.pow(1n+a, n))) : {_ == True{} : Bool}
2255  one_le_pow(n, a)
2256
2257# Adding on the left never decreases a natural: n <= m + n.
2258law le_add_left:
2259  for n: Nat
2260  for m: Nat
2261  le(n, Nat.add(m, n))
2262
2263def le_add_left(n, m):
2264  match m:
2265    case 0n:
2266      le_refl(n)
2267    case 1n++p:
2268      +n = n
2269      le_trans(n, Nat.add(p, n), 1n+Nat.add(p, n), le_add_left(n, p), le_succ(Nat.add(p, n)))
2270
2271# A common left summand cancels in a difference: (k + n) - (k + m) = n - m.
2272law add_sub_add_left:
2273  for k: Nat
2274  for -n: Nat
2275  for -m: Nat
2276  {Nat.sub(Nat.add(k, n), Nat.add(k, m)) == Nat.sub(n, m) : Nat}
2277
2278def add_sub_add_left(k, n, m):
2279  match k:
2280    case 0n:
2281      {==}
2282    case 1n+p:
2283      add_sub_add_left(p, n, m)
2284
2285# A common right summand cancels in a difference: (n + k) - (m + k) = n - m.
2286law add_sub_add_right:
2287  for n: Nat
2288  for k: Nat
2289  for m: Nat
2290  {Nat.sub(Nat.add(n, k), Nat.add(m, k)) == Nat.sub(n, m) : Nat}
2291
2292def add_sub_add_right(n, k, m):
2293  +n = n
2294  +k = k
2295  +m = m
2296  %add_comm(k, n) : {Nat.sub(_, Nat.add(m, k)) == Nat.sub(n, m) : Nat}
2297  %add_comm(k, m) : {Nat.sub(Nat.add(k, n), _) == Nat.sub(n, m) : Nat}
2298  add_sub_add_left(k, n, m)
2299
2300# Subtracting a part of the right summand: k <= m implies (n + m) - k = n + (m - k).
2301law add_sub_assoc:
2302  for k: Nat
2303  for m: Nat
2304  for h: le(k, m)
2305  for n: Nat
2306  {Nat.sub(Nat.add(n, m), k) == Nat.add(n, Nat.sub(m, k)) : Nat}
2307
2308def add_sub_assoc(k, m, h, n):
2309  +k = k
2310  +m = m
2311  +n = n
2312  %sub_add_cancel(m, k, h) : {Nat.sub(Nat.add(n, _), k) == Nat.add(n, Nat.sub(m, k)) : Nat}
2313  %add_assoc(n, Nat.sub(m, k), k) : {Nat.sub(_, k) == Nat.add(n, Nat.sub(m, k)) : Nat}
2314  add_sub_cancel(Nat.add(n, Nat.sub(m, k)), k)
2315
2316# Subtracting a difference from its minuend: m <= n implies n - (n - m) = m.
2317law sub_sub_self:
2318  for n: Nat
2319  for m: Nat
2320  for h: le(m, n)
2321  {Nat.sub(n, Nat.sub(n, m)) == m : Nat}
2322
2323def sub_sub_self(n, m, h):
2324  match n m:
2325    case 0n 0n:
2326      {==}
2327    case 0n 1n+q:
2328      Empty.absurd({Nat.sub(0n, Nat.sub(0n, 1n+q)) == 1n+q : Nat}, internal_false_ne_true(h))
2329    case 1n+p 0n:
2330      sub_self(p)
2331    case 1n++p 1n++q:
2332      Equal.trans(Nat, Nat.sub(1n+p, Nat.sub(p, q)), 1n+Nat.sub(p, Nat.sub(p, q)), 1n+q, succ_sub(p, Nat.sub(p, q), sub_le(p, q)), Equal.cong(Nat, Nat, x => 1n+x, Nat.sub(p, Nat.sub(p, q)), q, sub_sub_self(p, q, h)))
2333
2334# Multiplication distributes over subtraction on the right: (n - m) * k = n * k - m * k.
2335law sub_mul:
2336  for n: Nat
2337  for m: Nat
2338  for k: Nat
2339  {Nat.mul(Nat.sub(n, m), k) == Nat.sub(Nat.mul(n, k), Nat.mul(m, k)) : Nat}
2340
2341def sub_mul(n, m, k):
2342  match n m:
2343    case 0n _:
2344      {==}
2345    case 1n++p 0n:
2346      +k = k
2347      Equal.sym(Nat, Nat.sub(Nat.mul(1n+p, k), 0n), Nat.mul(1n+p, k), sub_zero(Nat.mul(1n+p, k)))
2348    case 1n++p 1n++q:
2349      +k = k
2350      %Equal.sym(Nat, Nat.sub(Nat.add(k, Nat.mul(p, k)), Nat.add(k, Nat.mul(q, k))), Nat.sub(Nat.mul(p, k), Nat.mul(q, k)), add_sub_add_left(k, Nat.mul(p, k), Nat.mul(q, k))) : {Nat.mul(Nat.sub(p, q), k) == _ : Nat}
2351      sub_mul(p, q, k)
2352
2353# Multiplication distributes over subtraction on the left: n * (m - k) = n * m - n * k.
2354law mul_sub:
2355  for n: Nat
2356  for m: Nat
2357  for k: Nat
2358  {Nat.mul(n, Nat.sub(m, k)) == Nat.sub(Nat.mul(n, m), Nat.mul(n, k)) : Nat}
2359
2360def mul_sub(n, m, k):
2361  +n = n
2362  +m = m
2363  +k = k
2364  %mul_comm(Nat.sub(m, k), n) : {_ == Nat.sub(Nat.mul(n, m), Nat.mul(n, k)) : Nat}
2365  %mul_comm(m, n) : {Nat.mul(Nat.sub(m, k), n) == Nat.sub(_, Nat.mul(n, k)) : Nat}
2366  %mul_comm(k, n) : {Nat.mul(Nat.sub(m, k), n) == Nat.sub(Nat.mul(m, n), _) : Nat}
2367  sub_mul(m, k, n)
2368
2369# The minimum is the smaller argument on the left: a <= b implies min a b = a.
2370law min_eq_left:
2371  for a: Nat
2372  for b: Nat
2373  for h: le(a, b)
2374  {Nat.min(a, b) == a : Nat}
2375
2376def min_eq_left(a, b, h):
2377  match a b:
2378    case 0n _:
2379      {==}
2380    case 1n+p 0n:
2381      Empty.absurd({Nat.min(1n+p, 0n) == 1n+p : Nat}, internal_false_ne_true(h))
2382    case 1n++p 1n+q:
2383      %min_eq_left(p, q, h) : {1n+Nat.min(p, q) == 1n+_ : Nat}
2384      {==}
2385
2386# The minimum is the smaller argument on the right: b <= a implies min a b = b.
2387law min_eq_right:
2388  for a: Nat
2389  for b: Nat
2390  for h: le(b, a)
2391  {Nat.min(a, b) == b : Nat}
2392
2393def min_eq_right(a, b, h):
2394  match a b:
2395    case 0n 0n:
2396      {==}
2397    case 0n 1n+q:
2398      Empty.absurd({Nat.min(0n, 1n+q) == 1n+q : Nat}, internal_false_ne_true(h))
2399    case 1n+p 0n:
2400      {==}
2401    case 1n+p 1n++q:
2402      %min_eq_right(p, q, h) : {1n+Nat.min(p, q) == 1n+_ : Nat}
2403      {==}
2404
2405# The maximum is the larger argument on the left: b <= a implies max a b = a.
2406law max_eq_left:
2407  for a: Nat
2408  for b: Nat
2409  for h: le(b, a)
2410  {Nat.max(a, b) == a : Nat}
2411
2412def max_eq_left(a, b, h):
2413  match a b:
2414    case 0n 0n:
2415      {==}
2416    case 0n 1n+q:
2417      Empty.absurd({Nat.max(0n, 1n+q) == 0n : Nat}, internal_false_ne_true(h))
2418    case 1n+p 0n:
2419      {==}
2420    case 1n++p 1n+q:
2421      %max_eq_left(p, q, h) : {1n+Nat.max(p, q) == 1n+_ : Nat}
2422      {==}
2423
2424# The maximum is the larger argument on the right: a <= b implies max a b = b.
2425law max_eq_right:
2426  for a: Nat
2427  for b: Nat
2428  for h: le(a, b)
2429  {Nat.max(a, b) == b : Nat}
2430
2431def max_eq_right(a, b, h):
2432  match a b:
2433    case 0n _:
2434      {==}
2435    case 1n+p 0n:
2436      Empty.absurd({Nat.max(1n+p, 0n) == 0n : Nat}, internal_false_ne_true(h))
2437    case 1n+p 1n++q:
2438      %max_eq_right(p, q, h) : {1n+Nat.max(p, q) == 1n+_ : Nat}
2439      {==}
2440
2441def internal_and_false_sym(x: Bool) -> {False{} == Bool.and(x, False{}) : Bool}:
2442  match x:
2443    case False{}:
2444      {==}
2445    case True{}:
2446      {==}
2447
2448def internal_and_true_sym(x: Bool) -> {x == Bool.and(x, True{}) : Bool}:
2449  match x:
2450    case False{}:
2451      {==}
2452    case True{}:
2453      {==}
2454
2455# A number is at most the minimum exactly when it is at most both: a <= min b c tests as a <= b and a <= c.
2456law le_min:
2457  for a: Nat
2458  for b: Nat
2459  for c: Nat
2460  {Nat.is_le(a, Nat.min(b, c)) == Bool.and(Nat.is_le(a, b), Nat.is_le(a, c)) : Bool}
2461
2462def le_min(a, b, c):
2463  match a b c:
2464    case 0n 0n 0n:
2465      {==}
2466    case 0n 0n 1n+r:
2467      {==}
2468    case 0n 1n+q 0n:
2469      {==}
2470    case 0n 1n+q 1n+r:
2471      {==}
2472    case 1n+p 0n _:
2473      {==}
2474    case 1n+p 1n+q 0n:
2475      internal_and_false_sym(Nat.is_le(p, q))
2476    case 1n+p 1n+q 1n+r:
2477      le_min(p, q, r)
2478
2479# The maximum is at most c exactly when both arguments are: max a b <= c tests as a <= c and b <= c.
2480law max_le:
2481  for a: Nat
2482  for b: Nat
2483  for c: Nat
2484  {Nat.is_le(Nat.max(a, b), c) == Bool.and(Nat.is_le(a, c), Nat.is_le(b, c)) : Bool}
2485
2486def max_le(a, b, c):
2487  match a b c:
2488    case 0n _ 0n:
2489      {==}
2490    case 0n _ 1n+r:
2491      {==}
2492    case 1n+p 0n 0n:
2493      {==}
2494    case 1n+p 0n 1n+r:
2495      internal_and_true_sym(Nat.is_le(p, r))
2496    case 1n+p 1n+q 0n:
2497      {==}
2498    case 1n+p 1n+q 1n+r:
2499      max_le(p, q, r)
2500
2501# Multiplying on the left preserves the order: a <= b implies k * a <= k * b.
2502law mul_le_mul_left:
2503  for a: Nat
2504  for b: Nat
2505  for k: Nat
2506  for h: le(a, b)
2507  le(Nat.mul(k, a), Nat.mul(k, b))
2508
2509def mul_le_mul_left(a, b, k, h):
2510  +a = a
2511  +b = b
2512  +k = k
2513  %mul_comm(a, k) : le(_, Nat.mul(k, b))
2514  %mul_comm(b, k) : le(Nat.mul(a, k), _)
2515  mul_le_mul_right(a, b, k, h)
2516
2517# Multiplying two bounded factors stays bounded: a <= c and b <= d imply a * b <= c * d.
2518law mul_le_mul:
2519  for a: Nat
2520  for b: Nat
2521  for c: Nat
2522  for d: Nat
2523  for h1: le(a, c)
2524  for h2: le(b, d)
2525  le(Nat.mul(a, b), Nat.mul(c, d))
2526
2527def mul_le_mul(a, b, c, d, h1, h2):
2528  +a = a
2529  +b = b
2530  +c = c
2531  +d = d
2532  le_trans(Nat.mul(a, b), Nat.mul(c, b), Nat.mul(c, d), mul_le_mul_right(a, c, b, h1), mul_le_mul_left(b, d, c, h2))
2533
2534# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
2535
2536# Zero is a right identity for addition: x + 0 = x, reversed to rewrite toward the simple side.
2537law add_zero_sym:
2538  for x: Nat
2539  {x == Nat.add(x, 0n) : Nat}
2540
2541def add_zero_sym(x):
2542  Equal.sym(Nat, Nat.add(x, 0n), x, add_zero(x))
2543
2544# Zero is a left identity for addition: 0 + x = x, reversed to rewrite toward the simple side.
2545law zero_add_sym:
2546  for -x: Nat
2547  {x == Nat.add(0n, x) : Nat}
2548
2549def zero_add_sym(x):
2550  Equal.sym(Nat, Nat.add(0n, x), x, zero_add(x))
2551
2552# Adding a successor on the right: n + (m + 1) = (n + m) + 1, reversed to rewrite toward the simple side.
2553law add_succ_sym:
2554  for n: Nat
2555  for -m: Nat
2556  {1n+Nat.add(n, m) == Nat.add(n, 1n+m) : Nat}
2557
2558def add_succ_sym(n, m):
2559  Equal.sym(Nat, Nat.add(n, 1n+m), 1n+Nat.add(n, m), add_succ(n, m))
2560
2561# Adding a successor on the left: (n + 1) + m = (n + m) + 1, reversed to rewrite toward the simple side.
2562law succ_add_sym:
2563  for -n: Nat
2564  for -m: Nat
2565  {1n+Nat.add(n, m) == Nat.add(1n+n, m) : Nat}
2566
2567def succ_add_sym(n, m):
2568  Equal.sym(Nat, Nat.add(1n+n, m), 1n+Nat.add(n, m), succ_add(n, m))
2569
2570# Addition is commutative: n + m = m + n, reversed to rewrite toward the simple side.
2571law add_comm_sym:
2572  for n: Nat
2573  for m: Nat
2574  {Nat.add(m, n) == Nat.add(n, m) : Nat}
2575
2576def add_comm_sym(n, m):
2577  Equal.sym(Nat, Nat.add(n, m), Nat.add(m, n), add_comm(n, m))
2578
2579# Addition is associative: (a + b) + c = a + (b + c), reversed to rewrite toward the simple side.
2580law add_assoc_sym:
2581  for a: Nat
2582  for -b: Nat
2583  for -c: Nat
2584  {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, b), c) : Nat}
2585
2586def add_assoc_sym(a, b, c):
2587  Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(a, Nat.add(b, c)), add_assoc(a, b, c))
2588
2589# Left commutativity of addition: a + (b + c) = b + (a + c), reversed to rewrite toward the simple side.
2590law add_left_comm_sym:
2591  for a: Nat
2592  for b: Nat
2593  for -c: Nat
2594  {Nat.add(b, Nat.add(a, c)) == Nat.add(a, Nat.add(b, c)) : Nat}
2595
2596def add_left_comm_sym(a, b, c):
2597  Equal.sym(Nat, Nat.add(a, Nat.add(b, c)), Nat.add(b, Nat.add(a, c)), add_left_comm(a, b, c))
2598
2599# Right commutativity of addition: (a + b) + c = (a + c) + b, reversed to rewrite toward the simple side.
2600law add_right_comm_sym:
2601  for a: Nat
2602  for b: Nat
2603  for c: Nat
2604  {Nat.add(Nat.add(a, c), b) == Nat.add(Nat.add(a, b), c) : Nat}
2605
2606def add_right_comm_sym(a, b, c):
2607  Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(Nat.add(a, c), b), add_right_comm(a, b, c))
2608
2609# Four-way regrouping of a sum: (a + b) + (c + d) = (a + c) + (b + d), reversed to rewrite toward the simple side.
2610law add_add_add_comm_sym:
2611  for a: Nat
2612  for b: Nat
2613  for c: Nat
2614  for -d: Nat
2615  {Nat.add(Nat.add(a, c), Nat.add(b, d)) == Nat.add(Nat.add(a, b), Nat.add(c, d)) : Nat}
2616
2617def add_add_add_comm_sym(a, b, c, d):
2618  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))
2619
2620# Zero absorbs multiplication on the right: x * 0 = 0, reversed to rewrite toward the simple side.
2621law mul_zero_sym:
2622  for x: Nat
2623  {0n == Nat.mul(x, 0n) : Nat}
2624
2625def mul_zero_sym(x):
2626  Equal.sym(Nat, Nat.mul(x, 0n), 0n, mul_zero(x))
2627
2628# Zero absorbs multiplication on the left: 0 * x = 0, reversed to rewrite toward the simple side.
2629law zero_mul_sym:
2630  for -x: Nat
2631  {0n == Nat.mul(0n, x) : Nat}
2632
2633def zero_mul_sym(x):
2634  Equal.sym(Nat, Nat.mul(0n, x), 0n, zero_mul(x))
2635
2636# One is a right identity for multiplication: x * 1 = x, reversed to rewrite toward the simple side.
2637law mul_one_sym:
2638  for x: Nat
2639  {x == Nat.mul(x, 1n) : Nat}
2640
2641def mul_one_sym(x):
2642  Equal.sym(Nat, Nat.mul(x, 1n), x, mul_one(x))
2643
2644# One is a left identity for multiplication: 1 * x = x, reversed to rewrite toward the simple side.
2645law one_mul_sym:
2646  for x: Nat
2647  {x == Nat.mul(1n, x) : Nat}
2648
2649def one_mul_sym(x):
2650  Equal.sym(Nat, Nat.mul(1n, x), x, one_mul(x))
2651
2652# Multiplying by a successor on the right: n * (m + 1) = n * m + n, reversed to rewrite toward the simple side.
2653law mul_succ_sym:
2654  for n: Nat
2655  for m: Nat
2656  {Nat.add(Nat.mul(n, m), n) == Nat.mul(n, 1n+m) : Nat}
2657
2658def mul_succ_sym(n, m):
2659  Equal.sym(Nat, Nat.mul(n, 1n+m), Nat.add(Nat.mul(n, m), n), mul_succ(n, m))
2660
2661# Multiplying by a successor on the left: (n + 1) * m = n * m + m, reversed to rewrite toward the simple side.
2662law succ_mul_sym:
2663  for n: Nat
2664  for m: Nat
2665  {Nat.add(Nat.mul(n, m), m) == Nat.mul(1n+n, m) : Nat}
2666
2667def succ_mul_sym(n, m):
2668  Equal.sym(Nat, Nat.mul(1n+n, m), Nat.add(Nat.mul(n, m), m), succ_mul(n, m))
2669
2670# Multiplication is commutative: n * m = m * n, reversed to rewrite toward the simple side.
2671law mul_comm_sym:
2672  for n: Nat
2673  for m: Nat
2674  {Nat.mul(m, n) == Nat.mul(n, m) : Nat}
2675
2676def mul_comm_sym(n, m):
2677  Equal.sym(Nat, Nat.mul(n, m), Nat.mul(m, n), mul_comm(n, m))
2678
2679# Multiplication distributes over addition on the right: (a + b) * c = a * c + b * c, reversed to rewrite toward the simple side.
2680law add_mul_sym:
2681  for a: Nat
2682  for -b: Nat
2683  for c: Nat
2684  {Nat.add(Nat.mul(a, c), Nat.mul(b, c)) == Nat.mul(Nat.add(a, b), c) : Nat}
2685
2686def add_mul_sym(a, b, c):
2687  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))
2688
2689# Multiplication distributes over addition on the left: a * (b + c) = a * b + a * c, reversed to rewrite toward the simple side.
2690law mul_add_sym:
2691  for a: Nat
2692  for b: Nat
2693  for c: Nat
2694  {Nat.add(Nat.mul(a, b), Nat.mul(a, c)) == Nat.mul(a, Nat.add(b, c)) : Nat}
2695
2696def mul_add_sym(a, b, c):
2697  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))
2698
2699# Multiplication is associative: (a * b) * c = a * (b * c), reversed to rewrite toward the simple side.
2700law mul_assoc_sym:
2701  for a: Nat
2702  for b: Nat
2703  for c: Nat
2704  {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(Nat.mul(a, b), c) : Nat}
2705
2706def mul_assoc_sym(a, b, c):
2707  Equal.sym(Nat, Nat.mul(Nat.mul(a, b), c), Nat.mul(a, Nat.mul(b, c)), mul_assoc(a, b, c))
2708
2709# Subtracting zero changes nothing: n - 0 = n, reversed to rewrite toward the simple side.
2710law sub_zero_sym:
2711  for n: Nat
2712  {n == Nat.sub(n, 0n) : Nat}
2713
2714def sub_zero_sym(n):
2715  Equal.sym(Nat, Nat.sub(n, 0n), n, sub_zero(n))
2716
2717# Truncated subtraction from zero is zero: 0 - n = 0, reversed to rewrite toward the simple side.
2718law zero_sub_sym:
2719  for n: Nat
2720  {0n == Nat.sub(0n, n) : Nat}
2721
2722def zero_sub_sym(n):
2723  Equal.sym(Nat, Nat.sub(0n, n), 0n, zero_sub(n))
2724
2725# A natural minus itself is zero: n - n = 0, reversed to rewrite toward the simple side.
2726law sub_self_sym:
2727  for n: Nat
2728  {0n == Nat.sub(n, n) : Nat}
2729
2730def sub_self_sym(n):
2731  Equal.sym(Nat, Nat.sub(n, n), 0n, sub_self(n))
2732
2733# Subtracting successors: (n + 1) - (m + 1) = n - m, reversed to rewrite toward the simple side.
2734law succ_sub_succ_sym:
2735  for -n: Nat
2736  for -m: Nat
2737  {Nat.sub(n, m) == Nat.sub(1n+n, 1n+m) : Nat}
2738
2739def succ_sub_succ_sym(n, m):
2740  Equal.sym(Nat, Nat.sub(1n+n, 1n+m), Nat.sub(n, m), succ_sub_succ(n, m))
2741
2742# Adding then subtracting m cancels: (n + m) - m = n, reversed to rewrite toward the simple side.
2743law add_sub_cancel_sym:
2744  for n: Nat
2745  for m: Nat
2746  {n == Nat.sub(Nat.add(n, m), m) : Nat}
2747
2748def add_sub_cancel_sym(n, m):
2749  Equal.sym(Nat, Nat.sub(Nat.add(n, m), m), n, add_sub_cancel(n, m))
2750
2751# Adding then subtracting n cancels: (n + m) - n = m, reversed to rewrite toward the simple side.
2752law add_sub_cancel_left_sym:
2753  for n: Nat
2754  for m: Nat
2755  {m == Nat.sub(Nat.add(n, m), n) : Nat}
2756
2757def add_sub_cancel_left_sym(n, m):
2758  Equal.sym(Nat, Nat.sub(Nat.add(n, m), n), m, add_sub_cancel_left(n, m))
2759
2760# Subtracting twice is subtracting the sum: (n - m) - k = n - (m + k), reversed to rewrite toward the simple side.
2761law sub_sub_sym:
2762  for n: Nat
2763  for m: Nat
2764  for k: Nat
2765  {Nat.sub(n, Nat.add(m, k)) == Nat.sub(Nat.sub(n, m), k) : Nat}
2766
2767def sub_sub_sym(n, m, k):
2768  Equal.sym(Nat, Nat.sub(Nat.sub(n, m), k), Nat.sub(n, Nat.add(m, k)), sub_sub(n, m, k))
2769
2770# The division equation, for a positive divisor 1 + b: (a / (1 + b)) * (1 + b) + a % (1 + b) = a, reversed to rewrite toward the simple side.
2771law div_mod_eq_sym:
2772  for +a: Nat
2773  for +b: Nat
2774  {a == Nat.add(Nat.mul(Nat.div(a, 1n+b), 1n+b), Nat.mod(a, 1n+b)) : Nat}
2775
2776def div_mod_eq_sym(a, b):
2777  Equal.sym(Nat, Nat.add(Nat.mul(Nat.div(a, 1n+b), 1n+b), Nat.mod(a, 1n+b)), a, div_mod_eq(a, b))
2778
2779# Adding the divisor adds one to the quotient: ((1 + b) + a) / (1 + b) = 1 + a / (1 + b), reversed to rewrite toward the simple side.
2780law add_div_left_sym:
2781  for +a: Nat
2782  for +b: Nat
2783  {1n+Nat.div(a, 1n+b) == Nat.div(Nat.add(1n+b, a), 1n+b) : Nat}
2784
2785def add_div_left_sym(a, b):
2786  Equal.sym(Nat, Nat.div(Nat.add(1n+b, a), 1n+b), 1n+Nat.div(a, 1n+b), add_div_left(a, b))
2787
2788# A quotient is compared by multiplying back: n <= a / (1 + b) tests as n * (1 + b) <= a, reversed to rewrite toward the simple side.
2789law le_div_iff_mul_le_sym:
2790  for n: Nat
2791  for +a: Nat
2792  for +b: Nat
2793  {Nat.is_le(Nat.mul(n, 1n+b), a) == Nat.is_le(n, Nat.div(a, 1n+b)) : Bool}
2794
2795def le_div_iff_mul_le_sym(n, a, b):
2796  Equal.sym(Bool, Nat.is_le(n, Nat.div(a, 1n+b)), Nat.is_le(Nat.mul(n, 1n+b), a), le_div_iff_mul_le(n, a, b))
2797
2798# Minimum is commutative, reversed to rewrite toward the simple side.
2799law min_comm_sym:
2800  for a: Nat
2801  for b: Nat
2802  {Nat.min(b, a) == Nat.min(a, b) : Nat}
2803
2804def min_comm_sym(a, b):
2805  Equal.sym(Nat, Nat.min(a, b), Nat.min(b, a), min_comm(a, b))
2806
2807# Maximum is commutative, reversed to rewrite toward the simple side.
2808law max_comm_sym:
2809  for a: Nat
2810  for b: Nat
2811  {Nat.max(b, a) == Nat.max(a, b) : Nat}
2812
2813def max_comm_sym(a, b):
2814  Equal.sym(Nat, Nat.max(a, b), Nat.max(b, a), max_comm(a, b))
2815
2816# The minimum of a natural and itself is itself, reversed to rewrite toward the simple side.
2817law min_self_sym:
2818  for a: Nat
2819  {a == Nat.min(a, a) : Nat}
2820
2821def min_self_sym(a):
2822  Equal.sym(Nat, Nat.min(a, a), a, min_self(a))
2823
2824# The maximum of a natural and itself is itself, reversed to rewrite toward the simple side.
2825law max_self_sym:
2826  for a: Nat
2827  {a == Nat.max(a, a) : Nat}
2828
2829def max_self_sym(a):
2830  Equal.sym(Nat, Nat.max(a, a), a, max_self(a))
2831
2832# The minimum with zero is zero: min(a, 0) = 0, reversed to rewrite toward the simple side.
2833law min_zero_sym:
2834  for a: Nat
2835  {0n == Nat.min(a, 0n) : Nat}
2836
2837def min_zero_sym(a):
2838  Equal.sym(Nat, Nat.min(a, 0n), 0n, min_zero(a))
2839
2840# The minimum with zero is zero: min(0, a) = 0, reversed to rewrite toward the simple side.
2841law zero_min_sym:
2842  for a: Nat
2843  {0n == Nat.min(0n, a) : Nat}
2844
2845def zero_min_sym(a):
2846  Equal.sym(Nat, Nat.min(0n, a), 0n, zero_min(a))
2847
2848# Zero is an identity for maximum: max(a, 0) = a, reversed to rewrite toward the simple side.
2849law max_zero_sym:
2850  for a: Nat
2851  {a == Nat.max(a, 0n) : Nat}
2852
2853def max_zero_sym(a):
2854  Equal.sym(Nat, Nat.max(a, 0n), a, max_zero(a))
2855
2856# Zero is an identity for maximum: max(0, a) = a, reversed to rewrite toward the simple side.
2857law zero_max_sym:
2858  for a: Nat
2859  {a == Nat.max(0n, a) : Nat}
2860
2861def zero_max_sym(a):
2862  Equal.sym(Nat, Nat.max(0n, a), a, zero_max(a))
2863
2864# Minimum is associative, reversed to rewrite toward the simple side.
2865law min_assoc_sym:
2866  for a: Nat
2867  for b: Nat
2868  for c: Nat
2869  {Nat.min(a, Nat.min(b, c)) == Nat.min(Nat.min(a, b), c) : Nat}
2870
2871def min_assoc_sym(a, b, c):
2872  Equal.sym(Nat, Nat.min(Nat.min(a, b), c), Nat.min(a, Nat.min(b, c)), min_assoc(a, b, c))
2873
2874# Maximum is associative, reversed to rewrite toward the simple side.
2875law max_assoc_sym:
2876  for a: Nat
2877  for b: Nat
2878  for c: Nat
2879  {Nat.max(a, Nat.max(b, c)) == Nat.max(Nat.max(a, b), c) : Nat}
2880
2881def max_assoc_sym(a, b, c):
2882  Equal.sym(Nat, Nat.max(Nat.max(a, b), c), Nat.max(a, Nat.max(b, c)), max_assoc(a, b, c))
2883
2884# The minimum plus the maximum is the sum: min(a, b) + max(a, b) = a + b, reversed to rewrite toward the simple side.
2885law min_add_max_sym:
2886  for a: Nat
2887  for b: Nat
2888  {Nat.add(a, b) == Nat.add(Nat.min(a, b), Nat.max(a, b)) : Nat}
2889
2890def min_add_max_sym(a, b):
2891  Equal.sym(Nat, Nat.add(Nat.min(a, b), Nat.max(a, b)), Nat.add(a, b), min_add_max(a, b))
2892
2893# Any natural to the power zero is one, reversed to rewrite toward the simple side.
2894law pow_zero_sym:
2895  for -a: Nat
2896  {1n == Nat.pow(a, 0n) : Nat}
2897
2898def pow_zero_sym(a):
2899  Equal.sym(Nat, Nat.pow(a, 0n), 1n, pow_zero(a))
2900
2901# A power with a successor exponent: a^(n+1) = a * a^n, reversed to rewrite toward the simple side.
2902law pow_succ_sym:
2903  for -a: Nat
2904  for -n: Nat
2905  {Nat.mul(a, Nat.pow(a, n)) == Nat.pow(a, 1n+n) : Nat}
2906
2907def pow_succ_sym(a, n):
2908  Equal.sym(Nat, Nat.pow(a, 1n+n), Nat.mul(a, Nat.pow(a, n)), pow_succ(a, n))
2909
2910# Any natural to the power one is itself, reversed to rewrite toward the simple side.
2911law pow_one_sym:
2912  for a: Nat
2913  {a == Nat.pow(a, 1n) : Nat}
2914
2915def pow_one_sym(a):
2916  Equal.sym(Nat, Nat.pow(a, 1n), a, pow_one(a))
2917
2918# One to any power is one, reversed to rewrite toward the simple side.
2919law one_pow_sym:
2920  for n: Nat
2921  {1n == Nat.pow(1n, n) : Nat}
2922
2923def one_pow_sym(n):
2924  Equal.sym(Nat, Nat.pow(1n, n), 1n, one_pow(n))
2925
2926# Exponents add under multiplication: a^(m+n) = a^m * a^n, reversed to rewrite toward the simple side.
2927law pow_add_sym:
2928  for a: Nat
2929  for m: Nat
2930  for n: Nat
2931  {Nat.mul(Nat.pow(a, m), Nat.pow(a, n)) == Nat.pow(a, Nat.add(m, n)) : Nat}
2932
2933def pow_add_sym(a, m, n):
2934  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))
2935
2936# Doubling is adding a natural to itself, reversed to rewrite toward the simple side.
2937law double_eq_add_sym:
2938  for n: Nat
2939  {Nat.add(n, n) == Nat.double(n) : Nat}
2940
2941def double_eq_add_sym(n):
2942  Equal.sym(Nat, Nat.double(n), Nat.add(n, n), double_eq_add(n))
2943
2944# Every natural tests equal to itself, reversed to rewrite toward the simple side.
2945law is_eq_refl_sym:
2946  for n: Nat
2947  {True{} == Nat.is_eq(n, n) : Bool}
2948
2949def is_eq_refl_sym(n):
2950  Equal.sym(Bool, Nat.is_eq(n, n), True{}, is_eq_refl(n))
2951
2952# The equality test is symmetric, reversed to rewrite toward the simple side.
2953law is_eq_comm_sym:
2954  for a: Nat
2955  for b: Nat
2956  {Nat.is_eq(b, a) == Nat.is_eq(a, b) : Bool}
2957
2958def is_eq_comm_sym(a, b):
2959  Equal.sym(Bool, Nat.is_eq(a, b), Nat.is_eq(b, a), is_eq_comm(a, b))
2960
2961# A >= b tests the same as b <= a, reversed to rewrite toward the simple side.
2962law is_ge_eq_is_le_sym:
2963  for a: Nat
2964  for b: Nat
2965  {Nat.is_le(b, a) == Nat.is_ge(a, b) : Bool}
2966
2967def is_ge_eq_is_le_sym(a, b):
2968  Equal.sym(Bool, Nat.is_ge(a, b), Nat.is_le(b, a), is_ge_eq_is_le(a, b))
2969
2970# A > b tests the same as b < a, reversed to rewrite toward the simple side.
2971law is_gt_eq_is_lt_sym:
2972  for a: Nat
2973  for b: Nat
2974  {Nat.is_lt(b, a) == Nat.is_gt(a, b) : Bool}
2975
2976def is_gt_eq_is_lt_sym(a, b):
2977  Equal.sym(Bool, Nat.is_gt(a, b), Nat.is_lt(b, a), is_gt_eq_is_lt(a, b))
2978
2979# A < b tests the same as a + 1 <= b, reversed to rewrite toward the simple side.
2980law is_lt_eq_succ_le_sym:
2981  for a: Nat
2982  for b: Nat
2983  {Nat.is_le(1n+a, b) == Nat.is_lt(a, b) : Bool}
2984
2985def is_lt_eq_succ_le_sym(a, b):
2986  Equal.sym(Bool, Nat.is_lt(a, b), Nat.is_le(1n+a, b), is_lt_eq_succ_le(a, b))
2987
2988# Not (a <= b) tests the same as b < a, reversed to rewrite toward the simple side.
2989law not_is_le_sym:
2990  for a: Nat
2991  for b: Nat
2992  {Nat.is_lt(b, a) == Bool.not(Nat.is_le(a, b)) : Bool}
2993
2994def not_is_le_sym(a, b):
2995  Equal.sym(Bool, Bool.not(Nat.is_le(a, b)), Nat.is_lt(b, a), not_is_le(a, b))
2996
2997# Not (a < b) tests the same as b <= a, reversed to rewrite toward the simple side.
2998law not_is_lt_sym:
2999  for a: Nat
3000  for b: Nat
3001  {Nat.is_le(b, a) == Bool.not(Nat.is_lt(a, b)) : Bool}
3002
3003def not_is_lt_sym(a, b):
3004  Equal.sym(Bool, Bool.not(Nat.is_lt(a, b)), Nat.is_le(b, a), not_is_lt(a, b))
3005
3006# Adding the same amount on the left does not change the order test: a <= b tests as k + a <= k + b, reversed to rewrite toward the simple side.
3007law add_le_add_iff_left_sym:
3008  for k: Nat
3009  for -a: Nat
3010  for -b: Nat
3011  {Nat.is_le(Nat.add(k, a), Nat.add(k, b)) == Nat.is_le(a, b) : Bool}
3012
3013def add_le_add_iff_left_sym(k, a, b):
3014  Equal.sym(Bool, Nat.is_le(a, b), Nat.is_le(Nat.add(k, a), Nat.add(k, b)), add_le_add_iff_left(k, a, b))
3015
3016# A sum is at most c exactly when a <= c and b <= c - a: a + b <= c tests as both, reversed to rewrite toward the simple side.
3017law le_and_le_sub_iff_add_le_sym:
3018  for a: Nat
3019  for -b: Nat
3020  for c: Nat
3021  {Nat.is_le(Nat.add(a, b), c) == Bool.and(Nat.is_le(a, c), Nat.is_le(b, Nat.sub(c, a))) : Bool}
3022
3023def le_and_le_sub_iff_add_le_sym(a, b, c):
3024  Equal.sym(Bool, Bool.and(Nat.is_le(a, c), Nat.is_le(b, Nat.sub(c, a))), Nat.is_le(Nat.add(a, b), c), le_and_le_sub_iff_add_le(a, b, c))
3025
3026# The minimum is at most c exactly when one argument is: min a b <= c tests as a <= c or b <= c, reversed to rewrite toward the simple side.
3027law min_le_iff_sym:
3028  for a: Nat
3029  for b: Nat
3030  for c: Nat
3031  {Bool.or(Nat.is_le(a, c), Nat.is_le(b, c)) == Nat.is_le(Nat.min(a, b), c) : Bool}
3032
3033def min_le_iff_sym(a, b, c):
3034  Equal.sym(Bool, Nat.is_le(Nat.min(a, b), c), Bool.or(Nat.is_le(a, c), Nat.is_le(b, c)), min_le_iff(a, b, c))
3035
3036# The maximum is above a exactly when one argument is: a < max b c tests as a < b or a < c, reversed to rewrite toward the simple side.
3037law lt_max_iff_sym:
3038  for a: Nat
3039  for b: Nat
3040  for c: Nat
3041  {Bool.or(Nat.is_lt(a, b), Nat.is_lt(a, c)) == Nat.is_lt(a, Nat.max(b, c)) : Bool}
3042
3043def lt_max_iff_sym(a, b, c):
3044  Equal.sym(Bool, Nat.is_lt(a, Nat.max(b, c)), Bool.or(Nat.is_lt(a, b), Nat.is_lt(a, c)), lt_max_iff(a, b, c))
3045
3046# Comparing against a difference is comparing the sum: a < c - b tests as b + a < c, reversed to rewrite toward the simple side.
3047law lt_sub_iff_add_lt_sym:
3048  for a: Nat
3049  for b: Nat
3050  for c: Nat
3051  {Nat.is_lt(Nat.add(b, a), c) == Nat.is_lt(a, Nat.sub(c, b)) : Bool}
3052
3053def lt_sub_iff_add_lt_sym(a, b, c):
3054  Equal.sym(Bool, Nat.is_lt(a, Nat.sub(c, b)), Nat.is_lt(Nat.add(b, a), c), lt_sub_iff_add_lt(a, b, c))
3055
3056# Zero divided by anything is zero: 0 / b = 0, reversed to rewrite toward the simple side.
3057law zero_div_sym:
3058  for b: Nat
3059  {0n == Nat.div(0n, b) : Nat}
3060
3061def zero_div_sym(b):
3062  Equal.sym(Nat, Nat.div(0n, b), 0n, zero_div(b))
3063
3064# Zero modulo anything is zero: 0 % b = 0, reversed to rewrite toward the simple side.
3065law zero_mod_sym:
3066  for b: Nat
3067  {0n == Nat.mod(0n, b) : Nat}
3068
3069def zero_mod_sym(b):
3070  Equal.sym(Nat, Nat.mod(0n, b), 0n, zero_mod(b))
3071
3072# Dividing by one changes nothing: a / 1 = a, reversed to rewrite toward the simple side.
3073law div_one_sym:
3074  for a: Nat
3075  {a == Nat.div(a, 1n) : Nat}
3076
3077def div_one_sym(a):
3078  Equal.sym(Nat, Nat.div(a, 1n), a, div_one(a))
3079
3080# Any natural modulo one is zero: a % 1 = 0, reversed to rewrite toward the simple side.
3081law mod_one_sym:
3082  for a: Nat
3083  {0n == Nat.mod(a, 1n) : Nat}
3084
3085def mod_one_sym(a):
3086  Equal.sym(Nat, Nat.mod(a, 1n), 0n, mod_one(a))
3087
3088# A natural modulo itself is zero: n % n = 0, reversed to rewrite toward the simple side.
3089law mod_self_sym:
3090  for n: Nat
3091  {0n == Nat.mod(n, n) : Nat}
3092
3093def mod_self_sym(n):
3094  Equal.sym(Nat, Nat.mod(n, n), 0n, mod_self(n))
3095
3096# A positive natural divided by itself is one: (1 + b) / (1 + b) = 1, reversed to rewrite toward the simple side.
3097law div_self_sym:
3098  for b: Nat
3099  {1n == Nat.div(1n+b, 1n+b) : Nat}
3100
3101def div_self_sym(b):
3102  Equal.sym(Nat, Nat.div(1n+b, 1n+b), 1n, div_self(b))
3103
3104# Taking a remainder twice is taking it once: (a % n) % n = a % n, reversed to rewrite toward the simple side.
3105law mod_mod_sym:
3106  for a: Nat
3107  for n: Nat
3108  {Nat.mod(a, n) == Nat.mod(Nat.mod(a, n), n) : Nat}
3109
3110def mod_mod_sym(a, n):
3111  Equal.sym(Nat, Nat.mod(Nat.mod(a, n), n), Nat.mod(a, n), mod_mod(a, n))
3112
3113# Adding the divisor does not change the remainder: (b + a) % b = a % b, reversed to rewrite toward the simple side.
3114law add_mod_left_sym:
3115  for a: Nat
3116  for b: Nat
3117  {Nat.mod(a, b) == Nat.mod(Nat.add(b, a), b) : Nat}
3118
3119def add_mod_left_sym(a, b):
3120  Equal.sym(Nat, Nat.mod(Nat.add(b, a), b), Nat.mod(a, b), add_mod_left(a, b))
3121
3122# Multiplying by a positive divisor then dividing by it cancels: (a * (1 + b)) / (1 + b) = a, reversed to rewrite toward the simple side.
3123law mul_div_cancel_sym:
3124  for a: Nat
3125  for b: Nat
3126  {a == Nat.div(Nat.mul(a, 1n+b), 1n+b) : Nat}
3127
3128def mul_div_cancel_sym(a, b):
3129  Equal.sym(Nat, Nat.div(Nat.mul(a, 1n+b), 1n+b), a, mul_div_cancel(a, b))
3130
3131# Multiplying on the left by a positive divisor then dividing by it cancels: ((1 + b) * a) / (1 + b) = a, reversed to rewrite toward the simple side.
3132law mul_div_cancel_left_sym:
3133  for a: Nat
3134  for b: Nat
3135  {a == Nat.div(Nat.mul(1n+b, a), 1n+b) : Nat}
3136
3137def mul_div_cancel_left_sym(a, b):
3138  Equal.sym(Nat, Nat.div(Nat.mul(1n+b, a), 1n+b), a, mul_div_cancel_left(a, b))
3139
3140# A multiple of b leaves no remainder modulo b: (a * b) % b = 0, reversed to rewrite toward the simple side.
3141law mul_mod_left_sym:
3142  for a: Nat
3143  for b: Nat
3144  {0n == Nat.mod(Nat.mul(a, b), b) : Nat}
3145
3146def mul_mod_left_sym(a, b):
3147  Equal.sym(Nat, Nat.mod(Nat.mul(a, b), b), 0n, mul_mod_left(a, b))
3148
3149# A multiple of a leaves no remainder modulo a: (a * b) % a = 0, reversed to rewrite toward the simple side.
3150law mul_mod_right_sym:
3151  for a: Nat
3152  for b: Nat
3153  {0n == Nat.mod(Nat.mul(a, b), a) : Nat}
3154
3155def mul_mod_right_sym(a, b):
3156  Equal.sym(Nat, Nat.mod(Nat.mul(a, b), a), 0n, mul_mod_right(a, b))
3157
3158# The remainder plus the divisor times the quotient is the dividend: a % b + b * (a / b) = a, reversed to rewrite toward the simple side.
3159law mod_add_div_sym:
3160  for a: Nat
3161  for b: Nat
3162  {a == Nat.add(Nat.mod(a, b), Nat.mul(b, Nat.div(a, b))) : Nat}
3163
3164def mod_add_div_sym(a, b):
3165  Equal.sym(Nat, Nat.add(Nat.mod(a, b), Nat.mul(b, Nat.div(a, b))), a, mod_add_div(a, b))
3166
3167# Left commutativity of multiplication: a * (b * c) = b * (a * c), reversed to rewrite toward the simple side.
3168law mul_left_comm_sym:
3169  for a: Nat
3170  for b: Nat
3171  for c: Nat
3172  {Nat.mul(b, Nat.mul(a, c)) == Nat.mul(a, Nat.mul(b, c)) : Nat}
3173
3174def mul_left_comm_sym(a, b, c):
3175  Equal.sym(Nat, Nat.mul(a, Nat.mul(b, c)), Nat.mul(b, Nat.mul(a, c)), mul_left_comm(a, b, c))
3176
3177# Right commutativity of multiplication: (a * b) * c = (a * c) * b, reversed to rewrite toward the simple side.
3178law mul_right_comm_sym:
3179  for a: Nat
3180  for b: Nat
3181  for c: Nat
3182  {Nat.mul(Nat.mul(a, c), b) == Nat.mul(Nat.mul(a, b), c) : Nat}
3183
3184def mul_right_comm_sym(a, b, c):
3185  Equal.sym(Nat, Nat.mul(Nat.mul(a, b), c), Nat.mul(Nat.mul(a, c), b), mul_right_comm(a, b, c))
3186
3187# Four-way regrouping of a product: (a * b) * (c * d) = (a * c) * (b * d), reversed to rewrite toward the simple side.
3188law mul_mul_mul_comm_sym:
3189  for a: Nat
3190  for b: Nat
3191  for c: Nat
3192  for d: Nat
3193  {Nat.mul(Nat.mul(a, c), Nat.mul(b, d)) == Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) : Nat}
3194
3195def mul_mul_mul_comm_sym(a, b, c, d):
3196  Equal.sym(Nat, Nat.mul(Nat.mul(a, b), Nat.mul(c, d)), Nat.mul(Nat.mul(a, c), Nat.mul(b, d)), mul_mul_mul_comm(a, b, c, d))
3197
3198# Zero to a positive power is zero: 0^(n+1) = 0, reversed to rewrite toward the simple side.
3199law zero_pow_sym:
3200  for -n: Nat
3201  {0n == Nat.pow(0n, 1n+n) : Nat}
3202
3203def zero_pow_sym(n):
3204  Equal.sym(Nat, Nat.pow(0n, 1n+n), 0n, zero_pow(n))
3205
3206# A power of a product is the product of the powers: (a * b)^n = a^n * b^n, reversed to rewrite toward the simple side.
3207law mul_pow_sym:
3208  for +a: Nat
3209  for +b: Nat
3210  for n: Nat
3211  {Nat.mul(Nat.pow(a, n), Nat.pow(b, n)) == Nat.pow(Nat.mul(a, b), n) : Nat}
3212
3213def mul_pow_sym(a, b, n):
3214  Equal.sym(Nat, Nat.pow(Nat.mul(a, b), n), Nat.mul(Nat.pow(a, n), Nat.pow(b, n)), mul_pow(a, b, n))
3215
3216# Exponents multiply under repeated powers: a^(m * n) = (a^m)^n, reversed to rewrite toward the simple side.
3217law pow_mul_sym:
3218  for a: Nat
3219  for m: Nat
3220  for n: Nat
3221  {Nat.pow(Nat.pow(a, m), n) == Nat.pow(a, Nat.mul(m, n)) : Nat}
3222
3223def pow_mul_sym(a, m, n):
3224  Equal.sym(Nat, Nat.pow(a, Nat.mul(m, n)), Nat.pow(Nat.pow(a, m), n), pow_mul(a, m, n))
3225
3226# A common left summand cancels in a difference: (k + n) - (k + m) = n - m, reversed to rewrite toward the simple side.
3227law add_sub_add_left_sym:
3228  for k: Nat
3229  for -n: Nat
3230  for -m: Nat
3231  {Nat.sub(n, m) == Nat.sub(Nat.add(k, n), Nat.add(k, m)) : Nat}
3232
3233def add_sub_add_left_sym(k, n, m):
3234  Equal.sym(Nat, Nat.sub(Nat.add(k, n), Nat.add(k, m)), Nat.sub(n, m), add_sub_add_left(k, n, m))
3235
3236# A common right summand cancels in a difference: (n + k) - (m + k) = n - m, reversed to rewrite toward the simple side.
3237law add_sub_add_right_sym:
3238  for n: Nat
3239  for k: Nat
3240  for m: Nat
3241  {Nat.sub(n, m) == Nat.sub(Nat.add(n, k), Nat.add(m, k)) : Nat}
3242
3243def add_sub_add_right_sym(n, k, m):
3244  Equal.sym(Nat, Nat.sub(Nat.add(n, k), Nat.add(m, k)), Nat.sub(n, m), add_sub_add_right(n, k, m))
3245
3246# Multiplication distributes over subtraction on the right: (n - m) * k = n * k - m * k, reversed to rewrite toward the simple side.
3247law sub_mul_sym:
3248  for n: Nat
3249  for m: Nat
3250  for k: Nat
3251  {Nat.sub(Nat.mul(n, k), Nat.mul(m, k)) == Nat.mul(Nat.sub(n, m), k) : Nat}
3252
3253def sub_mul_sym(n, m, k):
3254  Equal.sym(Nat, Nat.mul(Nat.sub(n, m), k), Nat.sub(Nat.mul(n, k), Nat.mul(m, k)), sub_mul(n, m, k))
3255
3256# Multiplication distributes over subtraction on the left: n * (m - k) = n * m - n * k, reversed to rewrite toward the simple side.
3257law mul_sub_sym:
3258  for n: Nat
3259  for m: Nat
3260  for k: Nat
3261  {Nat.sub(Nat.mul(n, m), Nat.mul(n, k)) == Nat.mul(n, Nat.sub(m, k)) : Nat}
3262
3263def mul_sub_sym(n, m, k):
3264  Equal.sym(Nat, Nat.mul(n, Nat.sub(m, k)), Nat.sub(Nat.mul(n, m), Nat.mul(n, k)), mul_sub(n, m, k))
3265
3266# A number is at most the minimum exactly when it is at most both: a <= min b c tests as a <= b and a <= c, reversed to rewrite toward the simple side.
3267law le_min_sym:
3268  for a: Nat
3269  for b: Nat
3270  for c: Nat
3271  {Bool.and(Nat.is_le(a, b), Nat.is_le(a, c)) == Nat.is_le(a, Nat.min(b, c)) : Bool}
3272
3273def le_min_sym(a, b, c):
3274  Equal.sym(Bool, Nat.is_le(a, Nat.min(b, c)), Bool.and(Nat.is_le(a, b), Nat.is_le(a, c)), le_min(a, b, c))
3275
3276# The maximum is at most c exactly when both arguments are: max a b <= c tests as a <= c and b <= c, reversed to rewrite toward the simple side.
3277law max_le_sym:
3278  for a: Nat
3279  for b: Nat
3280  for c: Nat
3281  {Bool.and(Nat.is_le(a, c), Nat.is_le(b, c)) == Nat.is_le(Nat.max(a, b), c) : Bool}
3282
3283def max_le_sym(a, b, c):
3284  Equal.sym(Bool, Nat.is_le(Nat.max(a, b), c), Bool.and(Nat.is_le(a, c), Nat.is_le(b, c)), max_le(a, b, c))