1	import Base
2	import ../../../spec/lib/common.bend as C
3	import ../../lib/nat.bend as N
4	import ../../lib/lemmas/proofs/nat_algebra.bend as NA
5	import ../../lib/logic.bend as L
6	import ../natural/arith.bend as NR
7	
8	# The width vocabulary of spec/lib/common.bend (shift, high, low, fits: k
9	# doublings or halvings, never a literal 2^k) against the powers of two, for
10	# a symbolic k. The shape is Mathlib's Nat.shiftLeft_eq / Nat.shiftRight_eq_div_pow
11	# / Nat.lt_pow_two_of_testBit (Mathlib.Data.Nat.Bits): a shift is a
12	# multiplication or division by 2^k.
13	
14	# half(n) < m exactly when n < 2m
15	def lt_half(+n: Nat, +m: Nat) -> {Nat.is_lt(C.half(n), m) == Nat.is_lt(n, Nat.double(m)) : Bool}:
16	  match n m:
17	    case 0n 0n:
18	      {==}
19	    case 0n 1n+mp:
20	      {==}
21	    case 1n 0n:
22	      {==}
23	    case 1n 1n+mp:
24	      {==}
25	    case 2n+ +q 0n:
26	      {==}
27	    case 2n+ +q 1n+ +mp:
28	      lt_half(q, mp)
29	
30	# fits(k, n) is n < 2^k
31	def fits_lt(+k: Nat, +n: Nat) -> {C.fits(k, n) == Nat.is_lt(n, C.pow2(k)) : Bool}:
32	  match k:
33	    case 0n:
34	      match n:
35	        case 0n:
36	          {==}
37	        case 1n+ +np:
38	          Equal.sym(Bool, Nat.is_lt(np, 0n), False{}, N.not_lt_zero(np))
39	    case 1n+ +p:
40	      %Equal.sym(Bool, C.fits(p, C.half(n)), Nat.is_lt(C.half(n), C.pow2(p)), fits_lt(p, C.half(n))) : {_ == Nat.is_lt(n, Nat.double(C.pow2(p))) : Bool}
41	      lt_half(n, C.pow2(p))
42	
43	# ---- n == bit(n) + 2 half(n), and the halves of r + 2 x ----
44	
45	def hb(+n: Nat) -> {n == Nat.add(C.bit(n), Nat.double(C.half(n))) : Nat}:
46	  match n:
47	    case 0n:
48	      {==}
49	    case 1n:
50	      {==}
51	    case 2n+ +q:
52	      +e = hb(q)
53	      Equal.trans(Nat, 2n+q, 2n+Nat.add(C.bit(q), Nat.double(C.half(q))), Nat.add(C.bit(q), 2n+Nat.double(C.half(q))), Equal.cong(Nat, Nat, t => 2n+t, q, Nat.add(C.bit(q), Nat.double(C.half(q))), e), Equal.sym(Nat, Nat.add(C.bit(q), 2n+Nat.double(C.half(q))), 2n+Nat.add(C.bit(q), Nat.double(C.half(q))), Equal.trans(Nat, Nat.add(C.bit(q), 2n+Nat.double(C.half(q))), 1n+Nat.add(C.bit(q), 1n+Nat.double(C.half(q))), 2n+Nat.add(C.bit(q), Nat.double(C.half(q))), NA.add_succ(C.bit(q), 1n+Nat.double(C.half(q))), Equal.cong(Nat, Nat, t => 1n+t, Nat.add(C.bit(q), 1n+Nat.double(C.half(q))), 1n+Nat.add(C.bit(q), Nat.double(C.half(q))), NA.add_succ(C.bit(q), Nat.double(C.half(q)))))))
54	
55	def half_dbl(+r: Nat, +x: Nat) -> {C.half(Nat.add(r, Nat.double(x))) == Nat.add(C.half(r), x) : Nat}:
56	  match r:
57	    case 0n:
58	      match x:
59	        case 0n:
60	          {==}
61	        case 1n+ +y:
62	          Equal.cong(Nat, Nat, t => 1n+t, C.half(Nat.double(y)), y, half_dbl(0n, y))
63	    case 1n:
64	      match x:
65	        case 0n:
66	          {==}
67	        case 1n+ +y:
68	          Equal.cong(Nat, Nat, t => 1n+t, C.half(1n+Nat.double(y)), y, half_dbl(1n, y))
69	    case 2n+ +s:
70	      Equal.cong(Nat, Nat, t => 1n+t, C.half(Nat.add(s, Nat.double(x))), Nat.add(C.half(s), x), half_dbl(s, x))
71	
72	def bit_dbl(+r: Nat, +x: Nat) -> {C.bit(Nat.add(r, Nat.double(x))) == C.bit(r) : Nat}:
73	  match r:
74	    case 0n:
75	      match x:
76	        case 0n:
77	          {==}
78	        case 1n+ +y:
79	          bit_dbl(0n, y)
80	    case 1n:
81	      match x:
82	        case 0n:
83	          {==}
84	        case 1n+ +y:
85	          bit_dbl(1n, y)
86	    case 2n+ +s:
87	      bit_dbl(s, x)
88	
89	# ---- n == low(k, n) + shift(k, high(k, n)), low(k, n) < 2^k, and uniqueness ----
90	
91	def low_high(+k: Nat, +n: Nat) -> {n == Nat.add(C.low(k, n), C.shift(k, C.high(k, n))) : Nat}:
92	  match k:
93	    case 0n:
94	      {==}
95	    case 1n+ +p:
96	      +h = C.half(n)
97	      +l = C.low(p, h)
98	      +s = C.shift(p, C.high(p, h))
99	      +e1 = Equal.trans(Nat, n, Nat.add(C.bit(n), Nat.double(h)), Nat.add(C.bit(n), Nat.double(Nat.add(l, s))), hb(n), Equal.cong(Nat, Nat, t => Nat.add(C.bit(n), Nat.double(t)), h, Nat.add(l, s), low_high(p, h)))
100	      +e2 = Equal.trans(Nat, Nat.add(C.bit(n), Nat.double(Nat.add(l, s))), Nat.add(C.bit(n), Nat.add(Nat.double(l), Nat.double(s))), Nat.add(Nat.add(C.bit(n), Nat.double(l)), Nat.double(s)), Equal.cong(Nat, Nat, t => Nat.add(C.bit(n), t), Nat.double(Nat.add(l, s)), Nat.add(Nat.double(l), Nat.double(s)), NA.double_add(l, s)), Equal.sym(Nat, Nat.add(Nat.add(C.bit(n), Nat.double(l)), Nat.double(s)), Nat.add(C.bit(n), Nat.add(Nat.double(l), Nat.double(s))), NA.add_assoc(C.bit(n), Nat.double(l), Nat.double(s))))
101	      Equal.trans(Nat, n, Nat.add(C.bit(n), Nat.double(Nat.add(l, s))), Nat.add(Nat.add(C.bit(n), Nat.double(l)), Nat.double(s)), e1, e2)
102	
103	def bit_le1(+n: Nat) -> {Nat.is_le(C.bit(n), 1n) == True{} : Bool}:
104	  match n:
105	    case 0n:
106	      {==}
107	    case 1n:
108	      {==}
109	    case 2n+ +q:
110	      bit_le1(q)
111	
112	def le_add_r(+a: Nat, +b: Nat, +c: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(Nat.add(a, c), Nat.add(b, c)) == True{} : Bool}:
113	  +h1 = L.subst(Nat, z => {Nat.is_le(z, Nat.add(c, b)) == True{} : Bool}, Nat.add(c, a), Nat.add(a, c), N.add_comm(c, a), N.le_add_left(a, b, c, h))
114	  L.subst(Nat, z => {Nat.is_le(Nat.add(a, c), z) == True{} : Bool}, Nat.add(c, b), Nat.add(b, c), N.add_comm(c, b), h1)
115	
116	def low_lt(+k: Nat, +n: Nat) -> {Nat.is_lt(C.low(k, n), C.pow2(k)) == True{} : Bool}:
117	  match k:
118	    case 0n:
119	      {==}
120	    case 1n+ +p:
121	      +l = C.low(p, C.half(n))
122	      +ih = low_lt(p, C.half(n))
123	      +b = C.bit(n)
124	      +hb1 = bit_le1(n)
125	      +h2 = N.lt_succ_le_succ(l, C.pow2(p), ih)
126	      +h3 = N.double_le(1n+l, C.pow2(p), h2)
127	      +h4 = L.subst(Nat, z => {Nat.is_le(z, Nat.double(C.pow2(p))) == True{} : Bool}, Nat.double(1n+l), Nat.add(2n, Nat.double(l)), N.double_succ(l), h3)
128	      +h5 = N.le_lt_trans(Nat.add(b, Nat.double(l)), Nat.add(1n, Nat.double(l)), Nat.add(2n, Nat.double(l)), le_add_r(b, 1n, Nat.double(l), hb1), N.lt_succ(1n+Nat.double(l)))
129	      N.lt_le_trans(Nat.add(b, Nat.double(l)), Nat.add(2n, Nat.double(l)), Nat.double(C.pow2(p)), h5, h4)
130	
131	# r < 2^k: low(k, r + shift(k, q)) == r and high(k, r + shift(k, q)) == q
132	def low_uniq(+k: Nat, +r: Nat, +q: Nat, +hr: {Nat.is_lt(r, C.pow2(k)) == True{} : Bool}) -> {C.low(k, Nat.add(r, C.shift(k, q))) == r : Nat}:
133	  match k:
134	    case 0n:
135	      match r:
136	        case 0n:
137	          {==}
138	        case 1n+ +rp:
139	          Empty.absurd({C.low(0n, Nat.add(1n+rp, C.shift(0n, q))) == 1n+rp : Nat}, N.lt_zero_absurd(rp, hr))
140	    case 1n+ +p:
141	      +eh = half_dbl(r, C.shift(p, q))
142	      +eb = bit_dbl(r, C.shift(p, q))
143	      +hr2 = Equal.trans(Bool, Nat.is_lt(C.half(r), C.pow2(p)), Nat.is_lt(r, Nat.double(C.pow2(p))), True{}, lt_half(r, C.pow2(p)), hr)
144	      +ih = low_uniq(p, C.half(r), q, hr2)
145	      +el = Equal.trans(Nat, C.low(p, C.half(Nat.add(r, Nat.double(C.shift(p, q))))), C.low(p, Nat.add(C.half(r), C.shift(p, q))), C.half(r), Equal.cong(Nat, Nat, t => C.low(p, t), C.half(Nat.add(r, Nat.double(C.shift(p, q)))), Nat.add(C.half(r), C.shift(p, q)), eh), ih)
146	      Equal.trans(Nat, Nat.add(C.bit(Nat.add(r, Nat.double(C.shift(p, q)))), Nat.double(C.low(p, C.half(Nat.add(r, Nat.double(C.shift(p, q))))))), Nat.add(C.bit(r), Nat.double(C.half(r))), r, Equal.trans(Nat, Nat.add(C.bit(Nat.add(r, Nat.double(C.shift(p, q)))), Nat.double(C.low(p, C.half(Nat.add(r, Nat.double(C.shift(p, q))))))), Nat.add(C.bit(r), Nat.double(C.low(p, C.half(Nat.add(r, Nat.double(C.shift(p, q))))))), Nat.add(C.bit(r), Nat.double(C.half(r))), Equal.cong(Nat, Nat, t => Nat.add(t, Nat.double(C.low(p, C.half(Nat.add(r, Nat.double(C.shift(p, q))))))), C.bit(Nat.add(r, Nat.double(C.shift(p, q)))), C.bit(r), eb), Equal.cong(Nat, Nat, t => Nat.add(C.bit(r), Nat.double(t)), C.low(p, C.half(Nat.add(r, Nat.double(C.shift(p, q))))), C.half(r), el)), Equal.sym(Nat, r, Nat.add(C.bit(r), Nat.double(C.half(r))), hb(r)))
147	
148	def high_uniq(+k: Nat, +r: Nat, +q: Nat, +hr: {Nat.is_lt(r, C.pow2(k)) == True{} : Bool}) -> {C.high(k, Nat.add(r, C.shift(k, q))) == q : Nat}:
149	  match k:
150	    case 0n:
151	      match r:
152	        case 0n:
153	          {==}
154	        case 1n+ +rp:
155	          Empty.absurd({C.high(0n, Nat.add(1n+rp, C.shift(0n, q))) == q : Nat}, N.lt_zero_absurd(rp, hr))
156	    case 1n+ +p:
157	      +eh = half_dbl(r, C.shift(p, q))
158	      +hr2 = Equal.trans(Bool, Nat.is_lt(C.half(r), C.pow2(p)), Nat.is_lt(r, Nat.double(C.pow2(p))), True{}, lt_half(r, C.pow2(p)), hr)
159	      Equal.trans(Nat, C.high(p, C.half(Nat.add(r, Nat.double(C.shift(p, q))))), C.high(p, Nat.add(C.half(r), C.shift(p, q))), q, Equal.cong(Nat, Nat, t => C.high(p, t), C.half(Nat.add(r, Nat.double(C.shift(p, q)))), Nat.add(C.half(r), C.shift(p, q)), eh), high_uniq(p, C.half(r), q, hr2))
160	
161	# ---- shift(k, x) is x 2^k ----
162	
163	def shift_zero(+k: Nat) -> {C.shift(k, 0n) == 0n : Nat}:
164	  match k:
165	    case 0n:
166	      {==}
167	    case 1n+ +p:
168	      Equal.cong(Nat, Nat, t => Nat.double(t), C.shift(p, 0n), 0n, shift_zero(p))
169	
170	def shift_add(+k: Nat, +x: Nat, +y: Nat) -> {C.shift(k, Nat.add(x, y)) == Nat.add(C.shift(k, x), C.shift(k, y)) : Nat}:
171	  match k:
172	    case 0n:
173	      {==}
174	    case 1n+ +p:
175	      Equal.trans(Nat, Nat.double(C.shift(p, Nat.add(x, y))), Nat.double(Nat.add(C.shift(p, x), C.shift(p, y))), Nat.add(Nat.double(C.shift(p, x)), Nat.double(C.shift(p, y))), Equal.cong(Nat, Nat, t => Nat.double(t), C.shift(p, Nat.add(x, y)), Nat.add(C.shift(p, x), C.shift(p, y)), shift_add(p, x, y)), NA.double_add(C.shift(p, x), C.shift(p, y)))
176	
177	def shift_one(+k: Nat) -> {C.shift(k, 1n) == C.pow2(k) : Nat}:
178	  match k:
179	    case 0n:
180	      {==}
181	    case 1n+ +p:
182	      Equal.cong(Nat, Nat, t => Nat.double(t), C.shift(p, 1n), C.pow2(p), shift_one(p))
183	
184	def shift_comp(+a: Nat, +b: Nat, +x: Nat) -> {C.shift(Nat.add(a, b), x) == C.shift(a, C.shift(b, x)) : Nat}:
185	  match a:
186	    case 0n:
187	      {==}
188	    case 1n+ +p:
189	      Equal.cong(Nat, Nat, t => Nat.double(t), C.shift(Nat.add(p, b), x), C.shift(p, C.shift(b, x)), shift_comp(p, b, x))
190	
191	def shift_mono(+k: Nat, +x: Nat, +y: Nat, +h: {Nat.is_le(x, y) == True{} : Bool}) -> {Nat.is_le(C.shift(k, x), C.shift(k, y)) == True{} : Bool}:
192	  match k:
193	    case 0n:
194	      h
195	    case 1n+ +p:
196	      N.double_le(C.shift(p, x), C.shift(p, y), shift_mono(p, x, y, h))
197	
198	# shift(a, 2^b) == 2^(a + b)
199	def shift_pow2(+a: Nat, +b: Nat) -> {C.shift(a, C.pow2(b)) == C.pow2(Nat.add(a, b)) : Nat}:
200	  match a:
201	    case 0n:
202	      {==}
203	    case 1n+ +p:
204	      Equal.cong(Nat, Nat, t => Nat.double(t), C.shift(p, C.pow2(b)), C.pow2(Nat.add(p, b)), shift_pow2(p, b))
205	
206	# r < 2^k, x < 2^j: r + shift(k, x) < 2^(k + j)
207	def two_limb_lt(+k: Nat, +j: Nat, +r: Nat, +x: Nat, +hr: {Nat.is_lt(r, C.pow2(k)) == True{} : Bool}, +hx: {Nat.is_lt(x, C.pow2(j)) == True{} : Bool}) -> {Nat.is_lt(Nat.add(r, C.shift(k, x)), C.pow2(Nat.add(k, j))) == True{} : Bool}:
208	  +h1 = N.lt_add_r2(r, C.pow2(k), C.shift(k, x), hr)
209	  +e1 = Equal.trans(Nat, Nat.add(C.pow2(k), C.shift(k, x)), Nat.add(C.shift(k, 1n), C.shift(k, x)), C.shift(k, 1n+x), Equal.cong(Nat, Nat, t => Nat.add(t, C.shift(k, x)), C.pow2(k), C.shift(k, 1n), Equal.sym(Nat, C.shift(k, 1n), C.pow2(k), shift_one(k))), Equal.sym(Nat, C.shift(k, Nat.add(1n, x)), Nat.add(C.shift(k, 1n), C.shift(k, x)), shift_add(k, 1n, x)))
210	  +h2 = L.subst(Nat, z => {Nat.is_lt(Nat.add(r, C.shift(k, x)), z) == True{} : Bool}, Nat.add(C.pow2(k), C.shift(k, x)), C.shift(k, 1n+x), e1, h1)
211	  +h3 = shift_mono(k, 1n+x, C.pow2(j), N.lt_succ_le_succ(x, C.pow2(j), hx))
212	  N.lt_le_trans(Nat.add(r, C.shift(k, x)), C.shift(k, 1n+x), C.pow2(Nat.add(k, j)), h2, L.subst(Nat, z => {Nat.is_le(C.shift(k, 1n+x), z) == True{} : Bool}, C.shift(k, C.pow2(j)), C.pow2(Nat.add(k, j)), shift_pow2(k, j), h3))
213	
214	# ---- the same in fits form (no pow2 in the statement, safe at k == 64) ----
215	
216	def lt_of_fits(+k: Nat, +r: Nat, +h: {C.fits(k, r) == True{} : Bool}) -> {Nat.is_lt(r, C.pow2(k)) == True{} : Bool}:
217	  Equal.trans(Bool, Nat.is_lt(r, C.pow2(k)), C.fits(k, r), True{}, Equal.sym(Bool, C.fits(k, r), Nat.is_lt(r, C.pow2(k)), fits_lt(k, r)), h)
218	
219	def fits_of_lt(+k: Nat, +r: Nat, +h: {Nat.is_lt(r, C.pow2(k)) == True{} : Bool}) -> {C.fits(k, r) == True{} : Bool}:
220	  Equal.trans(Bool, C.fits(k, r), Nat.is_lt(r, C.pow2(k)), True{}, fits_lt(k, r), h)
221	
222	def low_u(+k: Nat, +r: Nat, +q: Nat, +hr: {C.fits(k, r) == True{} : Bool}) -> {C.low(k, Nat.add(r, C.shift(k, q))) == r : Nat}:
223	  low_uniq(k, r, q, lt_of_fits(k, r, hr))
224	
225	def high_u(+k: Nat, +r: Nat, +q: Nat, +hr: {C.fits(k, r) == True{} : Bool}) -> {C.high(k, Nat.add(r, C.shift(k, q))) == q : Nat}:
226	  high_uniq(k, r, q, lt_of_fits(k, r, hr))
227	
228	def low_fits(+k: Nat, +n: Nat) -> {C.fits(k, C.low(k, n)) == True{} : Bool}:
229	  fits_of_lt(k, C.low(k, n), low_lt(k, n))
230	
231	# r fits k bits, x fits j bits: r + shift(k, x) fits k + j bits
232	def limbs_fit(+k: Nat, +j: Nat, +r: Nat, +x: Nat, +hr: {C.fits(k, r) == True{} : Bool}, +hx: {C.fits(j, x) == True{} : Bool}) -> {C.fits(Nat.add(k, j), Nat.add(r, C.shift(k, x))) == True{} : Bool}:
233	  fits_of_lt(Nat.add(k, j), Nat.add(r, C.shift(k, x)), two_limb_lt(k, j, r, x, lt_of_fits(k, r, hr), lt_of_fits(j, x, hx)))
234	
235	# shift(k, q) with q >= 1 does not fit k bits added to anything
236	def unfit_shift(+k: Nat, +r: Nat, +qp: Nat) -> {C.fits(k, Nat.add(r, C.shift(k, 1n+qp))) == False{} : Bool}:
237	  +h1 = N.le_trans(C.pow2(k), C.shift(k, 1n+qp), Nat.add(r, C.shift(k, 1n+qp)), L.subst(Nat, z => {Nat.is_le(z, C.shift(k, 1n+qp)) == True{} : Bool}, C.shift(k, 1n), C.pow2(k), shift_one(k), shift_mono(k, 1n, 1n+qp, N.zero_le(qp))), L.subst(Nat, z => {Nat.is_le(C.shift(k, 1n+qp), z) == True{} : Bool}, Nat.add(C.shift(k, 1n+qp), r), Nat.add(r, C.shift(k, 1n+qp)), N.add_comm(C.shift(k, 1n+qp), r), N.le_add_right(C.shift(k, 1n+qp), r)))
238	  Equal.trans(Bool, C.fits(k, Nat.add(r, C.shift(k, 1n+qp))), Nat.is_lt(Nat.add(r, C.shift(k, 1n+qp)), C.pow2(k)), False{}, fits_lt(k, Nat.add(r, C.shift(k, 1n+qp))), N.le_not_lt(Nat.add(r, C.shift(k, 1n+qp)), C.pow2(k), h1))
239	
240	def shift_ge(+k: Nat, +x: Nat) -> {Nat.is_le(x, C.shift(k, x)) == True{} : Bool}:
241	  match k:
242	    case 0n:
243	      N.le_refl(x)
244	    case 1n+ +p:
245	      N.le_trans(x, C.shift(p, x), Nat.double(C.shift(p, x)), shift_ge(p, x), N.double_self_le(C.shift(p, x)))
246	
247	# with a symbolic one == 1 (so no closed 2^k appears where these are used)
248	def unfit_one(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +r: Nat) -> {C.fits(k, Nat.add(r, C.shift(k, one))) == False{} : Bool}:
249	  L.subst(Nat, z => {C.fits(k, Nat.add(r, C.shift(k, z))) == False{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), unfit_shift(k, r, 0n))
250	
251	def lt_one(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +h: {C.fits(k, x) == True{} : Bool}) -> {Nat.is_lt(x, C.shift(k, one)) == True{} : Bool}:
252	  +h2 = L.subst(Nat, z => {Nat.is_lt(x, z) == True{} : Bool}, C.pow2(k), C.shift(k, 1n), Equal.sym(Nat, C.shift(k, 1n), C.pow2(k), shift_one(k)), lt_of_fits(k, x, h))
253	  L.subst(Nat, z => {Nat.is_lt(x, C.shift(k, z)) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), h2)
254	
255	def dbl_eq0(+z: Nat) -> {Nat.is_eq(Nat.double(z), 0n) == Nat.is_eq(z, 0n) : Bool}:
256	  match z:
257	    case 0n:
258	      {==}
259	    case 1n+ +w:
260	      L.subst(Nat, t => {Nat.is_eq(t, 0n) == False{} : Bool}, Nat.add(2n, Nat.double(w)), Nat.double(1n+w), Equal.sym(Nat, Nat.double(1n+w), Nat.add(2n, Nat.double(w)), N.double_succ(w)), {==})
261	
262	def shift_eq0(+k: Nat, +y: Nat) -> {Nat.is_eq(C.shift(k, y), 0n) == Nat.is_eq(y, 0n) : Bool}:
263	  match k:
264	    case 0n:
265	      {==}
266	    case 1n+ +p:
267	      Equal.trans(Bool, Nat.is_eq(Nat.double(C.shift(p, y)), 0n), Nat.is_eq(C.shift(p, y), 0n), Nat.is_eq(y, 0n), dbl_eq0(C.shift(p, y)), shift_eq0(p, y))
268	
269	# ---- comparing two-limb numbers x + shift(k, y), x fitting k bits ----
270	
271	def lt_cancel_l(+d: Nat, +x: Nat, +y: Nat) -> {Nat.is_lt(Nat.add(d, x), Nat.add(d, y)) == Nat.is_lt(x, y) : Bool}:
272	  match d:
273	    case 0n:
274	      {==}
275	    case 1n+ +e:
276	      lt_cancel_l(e, x, y)
277	
278	def lt_cancel_r(+x: Nat, +y: Nat, +s: Nat) -> {Nat.is_lt(Nat.add(x, s), Nat.add(y, s)) == Nat.is_lt(x, y) : Bool}:
279	  +e = Equal.trans(Bool, Nat.is_lt(Nat.add(x, s), Nat.add(y, s)), Nat.is_lt(Nat.add(s, x), Nat.add(y, s)), Nat.is_lt(Nat.add(s, x), Nat.add(s, y)), Equal.cong(Nat, Bool, t => Nat.is_lt(t, Nat.add(y, s)), Nat.add(x, s), Nat.add(s, x), N.add_comm(x, s)), Equal.cong(Nat, Bool, t => Nat.is_lt(Nat.add(s, x), t), Nat.add(y, s), Nat.add(s, y), N.add_comm(y, s)))
280	  Equal.trans(Bool, Nat.is_lt(Nat.add(x, s), Nat.add(y, s)), Nat.is_lt(Nat.add(s, x), Nat.add(s, y)), Nat.is_lt(x, y), e, lt_cancel_l(s, x, y))
281	
282	# y1 < y2: x1 + shift(k, y1) < x2 + shift(k, y2)
283	def lt_hi(+k: Nat, +x1: Nat, +y1: Nat, +x2: Nat, +y2: Nat, +hx1: {C.fits(k, x1) == True{} : Bool}, +h: {Nat.is_lt(y1, y2) == True{} : Bool}) -> {Nat.is_lt(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))) == True{} : Bool}:
284	  +h1 = L.subst(Nat, z => {Nat.is_lt(x1, z) == True{} : Bool}, C.pow2(k), C.shift(k, 1n), Equal.sym(Nat, C.shift(k, 1n), C.pow2(k), shift_one(k)), lt_of_fits(k, x1, hx1))
285	  +h2 = N.lt_add_r2(x1, C.shift(k, 1n), C.shift(k, y1), h1)
286	  +e2 = Equal.sym(Nat, C.shift(k, Nat.add(1n, y1)), Nat.add(C.shift(k, 1n), C.shift(k, y1)), shift_add(k, 1n, y1))
287	  +h3 = L.subst(Nat, z => {Nat.is_lt(Nat.add(x1, C.shift(k, y1)), z) == True{} : Bool}, Nat.add(C.shift(k, 1n), C.shift(k, y1)), C.shift(k, 1n+y1), e2, h2)
288	  +h4 = shift_mono(k, 1n+y1, y2, N.lt_succ_le_succ(y1, y2, h))
289	  +h5 = L.subst(Nat, z => {Nat.is_le(C.shift(k, y2), z) == True{} : Bool}, Nat.add(C.shift(k, y2), x2), Nat.add(x2, C.shift(k, y2)), N.add_comm(C.shift(k, y2), x2), N.le_add_right(C.shift(k, y2), x2))
290	  N.lt_le_trans(Nat.add(x1, C.shift(k, y1)), C.shift(k, 1n+y1), Nat.add(x2, C.shift(k, y2)), h3, N.le_trans(C.shift(k, 1n+y1), C.shift(k, y2), Nat.add(x2, C.shift(k, y2)), h4, h5))
291	
292	def lt_limbs_c(+k: Nat, +x1: Nat, +y1: Nat, +x2: Nat, +y2: Nat, +hx1: {C.fits(k, x1) == True{} : Bool}, +hx2: {C.fits(k, x2) == True{} : Bool}, +c: Bool, +d: Bool, +hc: {Nat.is_lt(y1, y2) == c : Bool}, +hd: {Nat.is_eq(y1, y2) == d : Bool}) -> {Bool.or(c, Bool.and(d, Nat.is_lt(x1, x2))) == Nat.is_lt(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))) : Bool}:
293	  match c d:
294	    case True{} _:
295	      Equal.sym(Bool, Nat.is_lt(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))), True{}, lt_hi(k, x1, y1, x2, y2, hx1, hc))
296	    case False{} True{}:
297	      +ey = N.eq_from_is_eq(y1, y2, hd)
298	      +e1 = L.subst(Nat, z => {Nat.is_lt(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, z))) == Nat.is_lt(x1, x2) : Bool}, y1, y2, ey, lt_cancel_r(x1, x2, C.shift(k, y1)))
299	      Equal.sym(Bool, Nat.is_lt(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))), Nat.is_lt(x1, x2), e1)
300	    case False{} False{}:
301	      +h21 = N.lt_or_eq(y2, y1, N.not_lt_le(y1, y2, hc), N.is_eq_sym_false(y1, y2, hd))
302	      +hb = lt_hi(k, x2, y2, x1, y1, hx2, h21)
303	      Equal.sym(Bool, Nat.is_lt(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))), False{}, N.le_not_lt(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2)), N.lt_le(Nat.add(x2, C.shift(k, y2)), Nat.add(x1, C.shift(k, y1)), hb)))
304	
305	def lt_limbs(+k: Nat, +x1: Nat, +y1: Nat, +x2: Nat, +y2: Nat, +hx1: {C.fits(k, x1) == True{} : Bool}, +hx2: {C.fits(k, x2) == True{} : Bool}) -> {Bool.or(Nat.is_lt(y1, y2), Bool.and(Nat.is_eq(y1, y2), Nat.is_lt(x1, x2))) == Nat.is_lt(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))) : Bool}:
306	  lt_limbs_c(k, x1, y1, x2, y2, hx1, hx2, Nat.is_lt(y1, y2), Nat.is_eq(y1, y2), {==}, {==})
307	
308	def eq_limbs_f(+k: Nat, +x1: Nat, +y1: Nat, +x2: Nat, +y2: Nat, +d1: Bool, +d2: Bool, +h1: {Nat.is_eq(x1, x2) == d1 : Bool}, +h2: {Nat.is_eq(y1, y2) == d2 : Bool}, +he: {Nat.is_eq(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))) == False{} : Bool}) -> {Bool.and(d1, d2) == False{} : Bool}:
309	  match d1 d2:
310	    case True{} True{}:
311	      +ex = N.eq_from_is_eq(x1, x2, h1)
312	      +ey = N.eq_from_is_eq(y1, y2, h2)
313	      +e = L.subst(Nat, z => {Nat.is_eq(Nat.add(x1, C.shift(k, y1)), Nat.add(z, C.shift(k, y1))) == False{} : Bool}, x2, x1, Equal.sym(Nat, x1, x2, ex), L.subst(Nat, z => {Nat.is_eq(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, z))) == False{} : Bool}, y2, y1, Equal.sym(Nat, y1, y2, ey), he))
314	      Empty.absurd({True{} == False{} : Bool}, L.false_true(Equal.trans(Bool, False{}, Nat.is_eq(Nat.add(x1, C.shift(k, y1)), Nat.add(x1, C.shift(k, y1))), True{}, Equal.sym(Bool, Nat.is_eq(Nat.add(x1, C.shift(k, y1)), Nat.add(x1, C.shift(k, y1))), False{}, e), N.is_eq_refl(Nat.add(x1, C.shift(k, y1))))))
315	    case True{} False{}:
316	      {==}
317	    case False{} _:
318	      {==}
319	
320	def eq_limbs_c(+k: Nat, +x1: Nat, +y1: Nat, +x2: Nat, +y2: Nat, +hx1: {C.fits(k, x1) == True{} : Bool}, +hx2: {C.fits(k, x2) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))) == c : Bool}) -> {Bool.and(Nat.is_eq(x1, x2), Nat.is_eq(y1, y2)) == c : Bool}:
321	  match c:
322	    case True{}:
323	      +e = N.eq_from_is_eq(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2)), hc)
324	      +ex = Equal.trans(Nat, x1, C.low(k, Nat.add(x1, C.shift(k, y1))), x2, Equal.sym(Nat, C.low(k, Nat.add(x1, C.shift(k, y1))), x1, low_u(k, x1, y1, hx1)), Equal.trans(Nat, C.low(k, Nat.add(x1, C.shift(k, y1))), C.low(k, Nat.add(x2, C.shift(k, y2))), x2, Equal.cong(Nat, Nat, t => C.low(k, t), Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2)), e), low_u(k, x2, y2, hx2)))
325	      +ey = Equal.trans(Nat, y1, C.high(k, Nat.add(x1, C.shift(k, y1))), y2, Equal.sym(Nat, C.high(k, Nat.add(x1, C.shift(k, y1))), y1, high_u(k, x1, y1, hx1)), Equal.trans(Nat, C.high(k, Nat.add(x1, C.shift(k, y1))), C.high(k, Nat.add(x2, C.shift(k, y2))), y2, Equal.cong(Nat, Nat, t => C.high(k, t), Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2)), e), high_u(k, x2, y2, hx2)))
326	      +a = L.subst(Nat, z => {Nat.is_eq(x1, z) == True{} : Bool}, x1, x2, ex, N.is_eq_refl(x1))
327	      +b = L.subst(Nat, z => {Nat.is_eq(y1, z) == True{} : Bool}, y1, y2, ey, N.is_eq_refl(y1))
328	      Equal.trans(Bool, Bool.and(Nat.is_eq(x1, x2), Nat.is_eq(y1, y2)), Bool.and(True{}, Nat.is_eq(y1, y2)), True{}, Equal.cong(Bool, Bool, t => Bool.and(t, Nat.is_eq(y1, y2)), Nat.is_eq(x1, x2), True{}, a), b)
329	    case False{}:
330	      eq_limbs_f(k, x1, y1, x2, y2, Nat.is_eq(x1, x2), Nat.is_eq(y1, y2), {==}, {==}, hc)
331	
332	def eq_limbs(+k: Nat, +x1: Nat, +y1: Nat, +x2: Nat, +y2: Nat, +hx1: {C.fits(k, x1) == True{} : Bool}, +hx2: {C.fits(k, x2) == True{} : Bool}) -> {Bool.and(Nat.is_eq(x1, x2), Nat.is_eq(y1, y2)) == Nat.is_eq(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))) : Bool}:
333	  eq_limbs_c(k, x1, y1, x2, y2, hx1, hx2, Nat.is_eq(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))), {==})
334	
335	# ---- parity: bit is mod 2, and shift(1 + p, y) is even ----
336	
337	def bit_mod(+n: Nat) -> {C.bit(n) == Nat.mod(n, 2n) : Nat}:
338	  match n:
339	    case 0n:
340	      {==}
341	    case 1n:
342	      {==}
343	    case 2n+ +q:
344	      Equal.trans(Nat, C.bit(q), Nat.mod(q, 2n), Nat.mod(2n+q, 2n), bit_mod(q), Equal.sym(Nat, Nat.mod(2n+q, 2n), Nat.mod(q, 2n), NR.absorb(1n, 1n, q)))
345	
346	def odd_limb(+p: Nat, +x: Nat, +y: Nat) -> {Nat.mod(Nat.add(x, C.shift(1n+p, y)), 2n) == Nat.mod(x, 2n) : Nat}:
347	  Equal.trans(Nat, Nat.mod(Nat.add(x, Nat.double(C.shift(p, y))), 2n), C.bit(Nat.add(x, Nat.double(C.shift(p, y)))), Nat.mod(x, 2n), Equal.sym(Nat, C.bit(Nat.add(x, Nat.double(C.shift(p, y)))), Nat.mod(Nat.add(x, Nat.double(C.shift(p, y))), 2n), bit_mod(Nat.add(x, Nat.double(C.shift(p, y))))), Equal.trans(Nat, C.bit(Nat.add(x, Nat.double(C.shift(p, y)))), C.bit(x), Nat.mod(x, 2n), bit_dbl(x, C.shift(p, y)), bit_mod(x)))
348	
349	# ---- halving a two-limb number ----
350	
351	def shift_dbl(+k: Nat, +z: Nat) -> {C.shift(k, Nat.double(z)) == Nat.double(C.shift(k, z)) : Nat}:
352	  match k:
353	    case 0n:
354	      {==}
355	    case 1n+ +p:
356	      Equal.cong(Nat, Nat, t => Nat.double(t), C.shift(p, Nat.double(z)), Nat.double(C.shift(p, z)), shift_dbl(p, z))
357	
358	def dbl_mul(+x: Nat, +y: Nat) -> {Nat.double(Nat.mul(x, y)) == Nat.mul(x, Nat.double(y)) : Nat}:
359	  Equal.trans(Nat, Nat.double(Nat.mul(x, y)), Nat.add(Nat.mul(x, y), Nat.mul(x, y)), Nat.mul(x, Nat.double(y)), NA.double_self(Nat.mul(x, y)), Equal.trans(Nat, Nat.add(Nat.mul(x, y), Nat.mul(x, y)), Nat.mul(x, Nat.add(y, y)), Nat.mul(x, Nat.double(y)), Equal.sym(Nat, Nat.mul(x, Nat.add(y, y)), Nat.add(Nat.mul(x, y), Nat.mul(x, y)), NA.mul_add_left(x, y, y)), Equal.cong(Nat, Nat, t => Nat.mul(x, t), Nat.add(y, y), Nat.double(y), Equal.sym(Nat, Nat.double(y), Nat.add(y, y), NA.double_self(y)))))
360	
361	def shift_mul(+k: Nat, +x: Nat) -> {C.shift(k, x) == Nat.mul(x, C.shift(k, 1n)) : Nat}:
362	  match k:
363	    case 0n:
364	      Equal.sym(Nat, Nat.mul(x, 1n), x, NA.mul_one(x))
365	    case 1n+ +p:
366	      Equal.trans(Nat, Nat.double(C.shift(p, x)), Nat.double(Nat.mul(x, C.shift(p, 1n))), Nat.mul(x, Nat.double(C.shift(p, 1n))), Equal.cong(Nat, Nat, t => Nat.double(t), C.shift(p, x), Nat.mul(x, C.shift(p, 1n)), shift_mul(p, x)), dbl_mul(x, C.shift(p, 1n)))
367	
368	# half(x + shift(1 + p, y)) == half(x) + bit(y) shift(p, one) + shift(1 + p, half(y))
369	def half_limbs(+p: Nat, +one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +y: Nat) -> {C.half(Nat.add(x, C.shift(1n+p, y))) == Nat.add(Nat.add(C.half(x), Nat.mul(C.bit(y), C.shift(p, one))), C.shift(1n+p, C.half(y))) : Nat}:
370	  +hx = C.half(x)
371	  +b = C.bit(y)
372	  +hy = C.half(y)
373	  +e1 = half_dbl(x, C.shift(p, y))
374	  +e2 = Equal.trans(Nat, C.shift(p, y), C.shift(p, Nat.add(b, Nat.double(hy))), Nat.add(C.shift(p, b), C.shift(p, Nat.double(hy))), Equal.cong(Nat, Nat, t => C.shift(p, t), y, Nat.add(b, Nat.double(hy)), hb(y)), shift_add(p, b, Nat.double(hy)))
375	  +e3 = Equal.trans(Nat, Nat.add(C.shift(p, b), C.shift(p, Nat.double(hy))), Nat.add(Nat.mul(b, C.shift(p, 1n)), C.shift(p, Nat.double(hy))), Nat.add(Nat.mul(b, C.shift(p, one)), Nat.double(C.shift(p, hy))), Equal.cong(Nat, Nat, t => Nat.add(t, C.shift(p, Nat.double(hy))), C.shift(p, b), Nat.mul(b, C.shift(p, 1n)), shift_mul(p, b)), Equal.trans(Nat, Nat.add(Nat.mul(b, C.shift(p, 1n)), C.shift(p, Nat.double(hy))), Nat.add(Nat.mul(b, C.shift(p, one)), C.shift(p, Nat.double(hy))), Nat.add(Nat.mul(b, C.shift(p, one)), Nat.double(C.shift(p, hy))), Equal.cong(Nat, Nat, t => Nat.add(Nat.mul(b, C.shift(p, t)), C.shift(p, Nat.double(hy))), 1n, one, Equal.sym(Nat, one, 1n, h1)), Equal.cong(Nat, Nat, t => Nat.add(Nat.mul(b, C.shift(p, one)), t), C.shift(p, Nat.double(hy)), Nat.double(C.shift(p, hy)), shift_dbl(p, hy))))
376	  +e4 = Equal.cong(Nat, Nat, t => Nat.add(hx, t), C.shift(p, y), Nat.add(Nat.mul(b, C.shift(p, one)), Nat.double(C.shift(p, hy))), Equal.trans(Nat, C.shift(p, y), Nat.add(C.shift(p, b), C.shift(p, Nat.double(hy))), Nat.add(Nat.mul(b, C.shift(p, one)), Nat.double(C.shift(p, hy))), e2, e3))
377	  Equal.trans(Nat, C.half(Nat.add(x, Nat.double(C.shift(p, y)))), Nat.add(hx, C.shift(p, y)), Nat.add(Nat.add(hx, Nat.mul(b, C.shift(p, one))), Nat.double(C.shift(p, hy))), e1, Equal.trans(Nat, Nat.add(hx, C.shift(p, y)), Nat.add(hx, Nat.add(Nat.mul(b, C.shift(p, one)), Nat.double(C.shift(p, hy)))), Nat.add(Nat.add(hx, Nat.mul(b, C.shift(p, one))), Nat.double(C.shift(p, hy))), e4, Equal.sym(Nat, Nat.add(Nat.add(hx, Nat.mul(b, C.shift(p, one))), Nat.double(C.shift(p, hy))), Nat.add(hx, Nat.add(Nat.mul(b, C.shift(p, one)), Nat.double(C.shift(p, hy)))), NA.add_assoc(hx, Nat.mul(b, C.shift(p, one)), Nat.double(C.shift(p, hy))))))
378	
379	def fits_one(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +h: {Nat.is_lt(x, C.shift(k, one)) == True{} : Bool}) -> {C.fits(k, x) == True{} : Bool}:
380	  +h2 = L.subst(Nat, z => {Nat.is_lt(x, C.shift(k, z)) == True{} : Bool}, one, 1n, h1, h)
381	  fits_of_lt(k, x, L.subst(Nat, z => {Nat.is_lt(x, z) == True{} : Bool}, C.shift(k, 1n), C.pow2(k), shift_one(k), h2))
382	
383	# a nonzero multiple of 2^k added: does not fit k bits
384	def unfit_nz(+k: Nat, +r: Nat, +q: Nat, +hq: {Nat.is_eq(q, 0n) == False{} : Bool}) -> {C.fits(k, Nat.add(r, C.shift(k, q))) == False{} : Bool}:
385	  match q:
386	    case 0n:
387	      Empty.absurd({C.fits(k, Nat.add(r, C.shift(k, 0n))) == False{} : Bool}, L.false_true(Equal.sym(Bool, True{}, False{}, hq)))
388	    case 1n+ +qp:
389	      unfit_shift(k, r, qp)
390	
391	# ---- products of two-limb numbers ----
392	
393	def shift_mul_l(+k: Nat, +x: Nat, +y: Nat) -> {Nat.mul(C.shift(k, x), y) == C.shift(k, Nat.mul(x, y)) : Nat}:
394	  +s1 = C.shift(k, 1n)
395	  Equal.trans(Nat, Nat.mul(C.shift(k, x), y), Nat.mul(Nat.mul(x, s1), y), C.shift(k, Nat.mul(x, y)), Equal.cong(Nat, Nat, t => Nat.mul(t, y), C.shift(k, x), Nat.mul(x, s1), shift_mul(k, x)), Equal.trans(Nat, Nat.mul(Nat.mul(x, s1), y), Nat.mul(x, Nat.mul(s1, y)), C.shift(k, Nat.mul(x, y)), NA.mul_assoc(x, s1, y), Equal.trans(Nat, Nat.mul(x, Nat.mul(s1, y)), Nat.mul(x, Nat.mul(y, s1)), C.shift(k, Nat.mul(x, y)), Equal.cong(Nat, Nat, t => Nat.mul(x, t), Nat.mul(s1, y), Nat.mul(y, s1), NA.mul_comm(s1, y)), Equal.trans(Nat, Nat.mul(x, Nat.mul(y, s1)), Nat.mul(Nat.mul(x, y), s1), C.shift(k, Nat.mul(x, y)), Equal.sym(Nat, Nat.mul(Nat.mul(x, y), s1), Nat.mul(x, Nat.mul(y, s1)), NA.mul_assoc(x, y, s1)), Equal.sym(Nat, C.shift(k, Nat.mul(x, y)), Nat.mul(Nat.mul(x, y), s1), shift_mul(k, Nat.mul(x, y)))))))
396	
397	def shift_mul_r(+k: Nat, +x: Nat, +y: Nat) -> {Nat.mul(x, C.shift(k, y)) == C.shift(k, Nat.mul(x, y)) : Nat}:
398	  Equal.trans(Nat, Nat.mul(x, C.shift(k, y)), Nat.mul(C.shift(k, y), x), C.shift(k, Nat.mul(x, y)), NA.mul_comm(x, C.shift(k, y)), Equal.trans(Nat, Nat.mul(C.shift(k, y), x), C.shift(k, Nat.mul(y, x)), C.shift(k, Nat.mul(x, y)), shift_mul_l(k, y, x), Equal.cong(Nat, Nat, t => C.shift(k, t), Nat.mul(y, x), Nat.mul(x, y), NA.mul_comm(y, x))))
399	
400	def low_add_shift(+k: Nat, +x: Nat, +y: Nat) -> {C.low(k, Nat.add(x, C.shift(k, y))) == C.low(k, x) : Nat}:
401	  +l = C.low(k, x)
402	  +h = C.high(k, x)
403	  +e = Equal.trans(Nat, Nat.add(x, C.shift(k, y)), Nat.add(Nat.add(l, C.shift(k, h)), C.shift(k, y)), Nat.add(l, C.shift(k, Nat.add(h, y))), Equal.cong(Nat, Nat, t => Nat.add(t, C.shift(k, y)), x, Nat.add(l, C.shift(k, h)), low_high(k, x)), Equal.trans(Nat, Nat.add(Nat.add(l, C.shift(k, h)), C.shift(k, y)), Nat.add(l, Nat.add(C.shift(k, h), C.shift(k, y))), Nat.add(l, C.shift(k, Nat.add(h, y))), NA.add_assoc(l, C.shift(k, h), C.shift(k, y)), Equal.cong(Nat, Nat, t => Nat.add(l, t), Nat.add(C.shift(k, h), C.shift(k, y)), C.shift(k, Nat.add(h, y)), Equal.sym(Nat, C.shift(k, Nat.add(h, y)), Nat.add(C.shift(k, h), C.shift(k, y)), shift_add(k, h, y)))))
404	  Equal.trans(Nat, C.low(k, Nat.add(x, C.shift(k, y))), C.low(k, Nat.add(l, C.shift(k, Nat.add(h, y)))), l, Equal.cong(Nat, Nat, t => C.low(k, t), Nat.add(x, C.shift(k, y)), Nat.add(l, C.shift(k, Nat.add(h, y))), e), low_u(k, l, Nat.add(h, y), low_fits(k, x)))
405	
406	def expand_k(+k: Nat, +al: Nat, +ah: Nat, +bl: Nat, +bh: Nat) -> {Nat.mul(Nat.add(al, C.shift(k, ah)), Nat.add(bl, C.shift(k, bh))) == Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, Nat.mul(al, bh))), Nat.add(C.shift(k, Nat.mul(ah, bl)), C.shift(k, C.shift(k, Nat.mul(ah, bh))))) : Nat}:
407	  Equal.trans(Nat, Nat.mul(Nat.add(al, C.shift(k, ah)), Nat.add(bl, C.shift(k, bh))), Nat.add(Nat.mul(al, Nat.add(bl, C.shift(k, bh))), Nat.mul(C.shift(k, ah), Nat.add(bl, C.shift(k, bh)))), Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, Nat.mul(al, bh))), Nat.add(C.shift(k, Nat.mul(ah, bl)), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), NA.mul_add_right(al, C.shift(k, ah), Nat.add(bl, C.shift(k, bh))), Equal.trans(Nat, Nat.add(Nat.mul(al, Nat.add(bl, C.shift(k, bh))), Nat.mul(C.shift(k, ah), Nat.add(bl, C.shift(k, bh)))), Nat.add(Nat.add(Nat.mul(al, bl), Nat.mul(al, C.shift(k, bh))), Nat.mul(C.shift(k, ah), Nat.add(bl, C.shift(k, bh)))), Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, Nat.mul(al, bh))), Nat.add(C.shift(k, Nat.mul(ah, bl)), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), Equal.cong(Nat, Nat, t => Nat.add(t, Nat.mul(C.shift(k, ah), Nat.add(bl, C.shift(k, bh)))), Nat.mul(al, Nat.add(bl, C.shift(k, bh))), Nat.add(Nat.mul(al, bl), Nat.mul(al, C.shift(k, bh))), NA.mul_add_left(al, bl, C.shift(k, bh))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(al, bl), Nat.mul(al, C.shift(k, bh))), Nat.mul(C.shift(k, ah), Nat.add(bl, C.shift(k, bh)))), Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, Nat.mul(al, bh))), Nat.mul(C.shift(k, ah), Nat.add(bl, C.shift(k, bh)))), Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, Nat.mul(al, bh))), Nat.add(C.shift(k, Nat.mul(ah, bl)), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), Equal.cong(Nat, Nat, t => Nat.add(Nat.add(Nat.mul(al, bl), t), Nat.mul(C.shift(k, ah), Nat.add(bl, C.shift(k, bh)))), Nat.mul(al, C.shift(k, bh)), C.shift(k, Nat.mul(al, bh)), shift_mul_r(k, al, bh)), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, Nat.mul(al, bh))), Nat.mul(C.shift(k, ah), Nat.add(bl, C.shift(k, bh)))), Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, Nat.mul(al, bh))), Nat.add(Nat.mul(C.shift(k, ah), bl), Nat.mul(C.shift(k, ah), C.shift(k, bh)))), Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, Nat.mul(al, bh))), Nat.add(C.shift(k, Nat.mul(ah, bl)), C.shift(k,
408	
409	# (al + 2^k ah)(bl + 2^k bh) == al bl + 2^k t + 2^(2k) (kc + ah bh) when al bh + ah bl == t + 2^k kc
410	def mul_k(+k: Nat, +al: Nat, +ah: Nat, +bl: Nat, +bh: Nat, +t: Nat, +kc: Nat, +e: {Nat.add(t, C.shift(k, kc)) == Nat.add(Nat.mul(al, bh), Nat.mul(ah, bl)) : Nat}) -> {Nat.mul(Nat.add(al, C.shift(k, ah)), Nat.add(bl, C.shift(k, bh))) == Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, t)), C.shift(k, C.shift(k, Nat.add(kc, Nat.mul(ah, bh))))) : Nat}:
411	  Equal.trans(Nat, Nat.mul(Nat.add(al, C.shift(k, ah)), Nat.add(bl, C.shift(k, bh))), Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, Nat.mul(al, bh))), Nat.add(C.shift(k, Nat.mul(ah, bl)), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, t)), C.shift(k, C.shift(k, Nat.add(kc, Nat.mul(ah, bh))))), expand_k(k, al, ah, bl, bh), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, Nat.mul(al, bh))), Nat.add(C.shift(k, Nat.mul(ah, bl)), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), Nat.add(Nat.mul(al, bl), Nat.add(C.shift(k, Nat.mul(al, bh)), Nat.add(C.shift(k, Nat.mul(ah, bl)), C.shift(k, C.shift(k, Nat.mul(ah, bh)))))), Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, t)), C.shift(k, C.shift(k, Nat.add(kc, Nat.mul(ah, bh))))), NA.add_assoc(Nat.mul(al, bl), C.shift(k, Nat.mul(al, bh)), Nat.add(C.shift(k, Nat.mul(ah, bl)), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), Equal.trans(Nat, Nat.add(Nat.mul(al, bl), Nat.add(C.shift(k, Nat.mul(al, bh)), Nat.add(C.shift(k, Nat.mul(ah, bl)), C.shift(k, C.shift(k, Nat.mul(ah, bh)))))), Nat.add(Nat.mul(al, bl), Nat.add(Nat.add(C.shift(k, Nat.mul(al, bh)), C.shift(k, Nat.mul(ah, bl))), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, t)), C.shift(k, C.shift(k, Nat.add(kc, Nat.mul(ah, bh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(al, bl), z), Nat.add(C.shift(k, Nat.mul(al, bh)), Nat.add(C.shift(k, Nat.mul(ah, bl)), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), Nat.add(Nat.add(C.shift(k, Nat.mul(al, bh)), C.shift(k, Nat.mul(ah, bl))), C.shift(k, C.shift(k, Nat.mul(ah, bh)))), Equal.sym(Nat, Nat.add(Nat.add(C.shift(k, Nat.mul(al, bh)), C.shift(k, Nat.mul(ah, bl))), C.shift(k, C.shift(k, Nat.mul(ah, bh)))), Nat.add(C.shift(k, Nat.mul(al, bh)), Nat.add(C.shift(k, Nat.mul(ah, bl)), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), NA.add_assoc(C.shift(k, Nat.mul(al, bh)), C.shift(k, Nat.mul(ah, bl)), C.shift(k, C.shift(k, Nat.mul(ah, bh)))))), Equal.trans(Nat, Nat.add(Nat.mul
412	
413	def low_fit(+k: Nat, +r: Nat, +hr: {C.fits(k, r) == True{} : Bool}) -> {C.low(k, r) == r : Nat}:
414	  +e = Equal.trans(Nat, Nat.add(r, C.shift(k, 0n)), Nat.add(r, 0n), r, Equal.cong(Nat, Nat, t => Nat.add(r, t), C.shift(k, 0n), 0n, shift_zero(k)), N.add_zero(r))
415	  L.subst(Nat, z => {C.low(k, z) == r : Nat}, Nat.add(r, C.shift(k, 0n)), r, e, low_u(k, r, 0n, hr))
416	
417	def pow2_sq(+k: Nat) -> {Nat.mul(C.pow2(k), C.pow2(k)) == C.pow2(Nat.add(k, k)) : Nat}:
418	  Equal.trans(Nat, Nat.mul(C.pow2(k), C.pow2(k)), Nat.mul(C.pow2(k), C.shift(k, 1n)), C.pow2(Nat.add(k, k)), Equal.cong(Nat, Nat, t => Nat.mul(C.pow2(k), t), C.pow2(k), C.shift(k, 1n), Equal.sym(Nat, C.shift(k, 1n), C.pow2(k), shift_one(k))), Equal.trans(Nat, Nat.mul(C.pow2(k), C.shift(k, 1n)), C.shift(k, C.pow2(k)), C.pow2(Nat.add(k, k)), Equal.sym(Nat, C.shift(k, C.pow2(k)), Nat.mul(C.pow2(k), C.shift(k, 1n)), shift_mul(k, C.pow2(k))), shift_pow2(k, k)))
419	
420	def shift_mul_one(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +x: Nat) -> {C.shift(k, x) == Nat.mul(x, C.shift(k, one)) : Nat}:
421	  L.subst(Nat, z => {C.shift(k, x) == Nat.mul(x, C.shift(k, z)) : Nat}, 1n, one, Equal.sym(Nat, one, 1n, h1), shift_mul(k, x))
422	
423	def shift_lt(+k: Nat, +a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_lt(C.shift(k, a), C.shift(k, b)) == True{} : Bool}:
424	  match k:
425	    case 0n:
426	      h
427	    case 1n+ +p:
428	      N.double_lt(C.shift(p, a), C.shift(p, b), shift_lt(p, a, b, h))
429	
430	# ---- shifting two-limb numbers ----
431	
432	def high_add_shift(+k: Nat, +x: Nat, +z: Nat) -> {C.high(k, Nat.add(x, C.shift(k, z))) == Nat.add(C.high(k, x), z) : Nat}:
433	  +l = C.low(k, x)
434	  +h = C.high(k, x)
435	  +e = Equal.trans(Nat, Nat.add(x, C.shift(k, z)), Nat.add(Nat.add(l, C.shift(k, h)), C.shift(k, z)), Nat.add(l, C.shift(k, Nat.add(h, z))), Equal.cong(Nat, Nat, t => Nat.add(t, C.shift(k, z)), x, Nat.add(l, C.shift(k, h)), low_high(k, x)), Equal.trans(Nat, Nat.add(Nat.add(l, C.shift(k, h)), C.shift(k, z)), Nat.add(l, Nat.add(C.shift(k, h), C.shift(k, z))), Nat.add(l, C.shift(k, Nat.add(h, z))), NA.add_assoc(l, C.shift(k, h), C.shift(k, z)), Equal.cong(Nat, Nat, t => Nat.add(l, t), Nat.add(C.shift(k, h), C.shift(k, z)), C.shift(k, Nat.add(h, z)), Equal.sym(Nat, C.shift(k, Nat.add(h, z)), Nat.add(C.shift(k, h), C.shift(k, z)), shift_add(k, h, z)))))
436	  Equal.trans(Nat, C.high(k, Nat.add(x, C.shift(k, z))), C.high(k, Nat.add(l, C.shift(k, Nat.add(h, z)))), Nat.add(h, z), Equal.cong(Nat, Nat, t => C.high(k, t), Nat.add(x, C.shift(k, z)), Nat.add(l, C.shift(k, Nat.add(h, z))), e), high_u(k, l, Nat.add(h, z), low_fits(k, x)))
437	
438	def high_comp(+a: Nat, +b: Nat, +n: Nat) -> {C.high(Nat.add(b, a), n) == C.high(a, C.high(b, n)) : Nat}:
439	  match b:
440	    case 0n:
441	      {==}
442	    case 1n+ +p:
443	      high_comp(a, p, C.half(n))
444	
445	# high(k, n) is n div 2^k, low(k, n) is n mod 2^k
446	def high_div(+k: Nat, +n: Nat, +pp: Nat, +hp: {C.pow2(k) == 1n+pp : Nat}) -> {C.high(k, n) == Nat.div(n, 1n+pp) : Nat}:
447	  +l = C.low(k, n)
448	  +h = C.high(k, n)
449	  +eS = Equal.trans(Nat, C.shift(k, h), Nat.mul(h, C.shift(k, 1n)), Nat.mul(h, 1n+pp), shift_mul(k, h), Equal.cong(Nat, Nat, t => Nat.mul(h, t), C.shift(k, 1n), 1n+pp, Equal.trans(Nat, C.shift(k, 1n), C.pow2(k), 1n+pp, shift_one(k), hp)))
450	  +e = Equal.trans(Nat, Nat.add(Nat.mul(h, 1n+pp), l), Nat.add(l, Nat.mul(h, 1n+pp)), n, N.add_comm(Nat.mul(h, 1n+pp), l), Equal.trans(Nat, Nat.add(l, Nat.mul(h, 1n+pp)), Nat.add(l, C.shift(k, h)), n, Equal.cong(Nat, Nat, t => Nat.add(l, t), Nat.mul(h, 1n+pp), C.shift(k, h), Equal.sym(Nat, C.shift(k, h), Nat.mul(h, 1n+pp), eS)), Equal.sym(Nat, n, Nat.add(l, C.shift(k, h)), low_high(k, n))))
451	  +hl = L.subst(Nat, t => {Nat.is_lt(l, t) == True{} : Bool}, C.pow2(k), 1n+pp, hp, low_lt(k, n))
452	  Equal.trans(Nat, h, Nat.div(Nat.add(Nat.mul(h, 1n+pp), l), 1n+pp), Nat.div(n, 1n+pp), Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(h, 1n+pp), l), 1n+pp), h, NR.div_of(h, pp, l, hl)), Equal.cong(Nat, Nat, t => Nat.div(t, 1n+pp), Nat.add(Nat.mul(h, 1n+pp), l), n, e))
453	
454	# low(s + t, shift(s, y)) == shift(s, low(t, y))
455	def low_shift(+s: Nat, +t: Nat, +y: Nat) -> {C.low(Nat.add(s, t), C.shift(s, y)) == C.shift(s, C.low(t, y)) : Nat}:
456	  +l = C.low(t, y)
457	  +h = C.high(t, y)
458	  +e = Equal.trans(Nat, C.shift(s, y), C.shift(s, Nat.add(l, C.shift(t, h))), Nat.add(C.shift(s, l), C.shift(Nat.add(s, t), h)), Equal.cong(Nat, Nat, z => C.shift(s, z), y, Nat.add(l, C.shift(t, h)), low_high(t, y)), Equal.trans(Nat, C.shift(s, Nat.add(l, C.shift(t, h))), Nat.add(C.shift(s, l), C.shift(s, C.shift(t, h))), Nat.add(C.shift(s, l), C.shift(Nat.add(s, t), h)), shift_add(s, l, C.shift(t, h)), Equal.cong(Nat, Nat, z => Nat.add(C.shift(s, l), z), C.shift(s, C.shift(t, h)), C.shift(Nat.add(s, t), h), Equal.sym(Nat, C.shift(Nat.add(s, t), h), C.shift(s, C.shift(t, h)), shift_comp(s, t, h)))))
459	  +hf = fits_of_lt(Nat.add(s, t), C.shift(s, l), L.subst(Nat, z => {Nat.is_lt(C.shift(s, l), z) == True{} : Bool}, C.shift(s, C.pow2(t)), C.pow2(Nat.add(s, t)), shift_pow2(s, t), shift_lt(s, l, C.pow2(t), low_lt(t, y))))
460	  Equal.trans(Nat, C.low(Nat.add(s, t), C.shift(s, y)), C.low(Nat.add(s, t), Nat.add(C.shift(s, l), C.shift(Nat.add(s, t), h))), C.shift(s, l), Equal.cong(Nat, Nat, z => C.low(Nat.add(s, t), z), C.shift(s, y), Nat.add(C.shift(s, l), C.shift(Nat.add(s, t), h)), e), low_u(Nat.add(s, t), C.shift(s, l), h, hf))
461	
462	# a < b, c <= a: a - c < b - c
463	def sub_lt_sub(+a: Nat, +b: Nat, +c: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}, +hc: {Nat.is_le(c, a) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(a, c), Nat.sub(b, c)) == True{} : Bool}:
464	  +ea = N.sub_add(a, c, hc)
465	  +eb = N.sub_add(b, c, N.le_trans(c, a, b, hc, N.lt_le(a, b, h)))
466	  +h2 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(c, Nat.sub(b, c))) == True{} : Bool}, a, Nat.add(c, Nat.sub(a, c)), Equal.sym(Nat, Nat.add(c, Nat.sub(a, c)), a, ea), L.subst(Nat, z => {Nat.is_lt(a, z) == True{} : Bool}, b, Nat.add(c, Nat.sub(b, c)), Equal.sym(Nat, Nat.add(c, Nat.sub(b, c)), b, eb), h))
467	  Equal.trans(Bool, Nat.is_lt(Nat.sub(a, c), Nat.sub(b, c)), Nat.is_lt(Nat.add(c, Nat.sub(a, c)), Nat.add(c, Nat.sub(b, c))), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(c, Nat.sub(a, c)), Nat.add(c, Nat.sub(b, c))), Nat.is_lt(Nat.sub(a, c), Nat.sub(b, c)), lt_cancel_l(c, Nat.sub(a, c), Nat.sub(b, c))), h2)