1	import Base
2	import ./logic.bend as L
3	import ./lemmas/proofs/nat_algebra.bend as NA
4	import ../../spec/lib/common.bend as SC
5	import ./lemmas/spec/numeric.bend as S
6	
7	# Natural-number order and arithmetic facts on Base Nat (Bool-valued
8	# comparisons), proved by induction on the installed definitions.
9	
10	def pred(n: Nat) -> Nat:
11	  match n:
12	    case 0n:
13	      0n
14	    case 1n+p:
15	      p
16	
17	def succ_inj(+a: Nat, +b: Nat, e: {1n+a == 1n+b : Nat}) -> {a == b : Nat}:
18	  Equal.cong(Nat, Nat, pred, 1n+a, 1n+b, e)
19	
20	def succ_cong(+a: Nat, +b: Nat, e: {a == b : Nat}) -> {1n+a == 1n+b : Nat}:
21	  Equal.cong(Nat, Nat, x => 1n+x, a, b, e)
22	
23	def is_zero(n: Nat) -> Bool:
24	  match n:
25	    case 0n:
26	      True{}
27	    case 1n+p:
28	      False{}
29	
30	def zero_succ(+n: Nat, e: {0n == 1n+n : Nat}) -> Empty:
31	  %e : L.truth(is_zero(_))
32	  Unit{}
33	
34	def succ_zero(+n: Nat, e: {1n+n == 0n : Nat}) -> Empty:
35	  zero_succ(n, Equal.sym(Nat, 1n+n, 0n, e))
36	
37	def add_zero(+n: Nat) -> {Nat.add(n, 0n) == n : Nat}:
38	  NA.add_zero(n)
39	
40	def add_succ(+a: Nat, +b: Nat) -> {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}:
41	  NA.add_succ(a, b)
42	
43	def add_comm(+a: Nat, +b: Nat) -> {Nat.add(a, b) == Nat.add(b, a) : Nat}:
44	  NA.add_comm(a, b)
45	
46	def add_assoc(+a: Nat, +b: Nat, +c: Nat) -> {Nat.add(Nat.add(a, b), c) == Nat.add(a, Nat.add(b, c)) : Nat}:
47	  NA.add_assoc(a, b, c)
48	
49	# ---- order ----
50	
51	def lt_irrefl(+n: Nat) -> {Nat.is_lt(n, n) == False{} : Bool}:
52	  match n:
53	    case 0n:
54	      {==}
55	    case 1n+p:
56	      lt_irrefl(p)
57	
58	def le_refl(+n: Nat) -> {Nat.is_le(n, n) == True{} : Bool}:
59	  match n:
60	    case 0n:
61	      {==}
62	    case 1n+p:
63	      le_refl(p)
64	
65	def lt_succ(+n: Nat) -> {Nat.is_lt(n, 1n+n) == True{} : Bool}:
66	  match n:
67	    case 0n:
68	      {==}
69	    case 1n+p:
70	      lt_succ(p)
71	
72	def le_succ(+n: Nat) -> {Nat.is_le(n, 1n+n) == True{} : Bool}:
73	  match n:
74	    case 0n:
75	      {==}
76	    case 1n+p:
77	      le_succ(p)
78	
79	def zero_le(+n: Nat) -> {Nat.is_le(0n, n) == True{} : Bool}:
80	  match n:
81	    case 0n:
82	      {==}
83	    case 1n+p:
84	      {==}
85	
86	def not_lt_zero(+n: Nat) -> {Nat.is_lt(n, 0n) == False{} : Bool}:
87	  match n:
88	    case 0n:
89	      {==}
90	    case 1n+p:
91	      {==}
92	
93	def lt_zero_absurd(+n: Nat, e: {Nat.is_lt(n, 0n) == True{} : Bool}) -> Empty:
94	  L.false_true(Equal.trans(Bool, False{}, Nat.is_lt(n, 0n), True{}, Equal.sym(Bool, Nat.is_lt(n, 0n), False{}, not_lt_zero(n)), e))
95	
96	def lt_le(+a: Nat, +b: Nat, e: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_le(a, b) == True{} : Bool}:
97	  match a b:
98	    case 0n 0n:
99	      {==}
100	    case 0n 1n+q:
101	      {==}
102	    case 1n+p 0n:
103	      Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, L.false_true(e))
104	    case 1n+p 1n+q:
105	      lt_le(p, q, e)
106	
107	def le_lt_succ(+a: Nat, +b: Nat, e: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_lt(a, 1n+b) == True{} : Bool}:
108	  match a b:
109	    case 0n _:
110	      {==}
111	    case 1n+p 0n:
112	      Empty.absurd({Nat.is_lt(1n+p, 1n) == True{} : Bool}, L.false_true(e))
113	    case 1n+p 1n+q:
114	      le_lt_succ(p, q, e)
115	
116	def lt_succ_le(+a: Nat, +b: Nat, e: {Nat.is_lt(a, 1n+b) == True{} : Bool}) -> {Nat.is_le(a, b) == True{} : Bool}:
117	  match a b:
118	    case 0n _:
119	      zero_le(b)
120	    case 1n+p 0n:
121	      Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, lt_zero_absurd(p, e))
122	    case 1n+p 1n+q:
123	      lt_succ_le(p, q, e)
124	
125	def succ_le_lt(+a: Nat, +b: Nat, e: {Nat.is_le(1n+a, b) == True{} : Bool}) -> {Nat.is_lt(a, b) == True{} : Bool}:
126	  match a b:
127	    case _ 0n:
128	      Empty.absurd({Nat.is_lt(a, 0n) == True{} : Bool}, L.false_true(e))
129	    case 0n 1n+q:
130	      {==}
131	    case 1n+p 1n+q:
132	      succ_le_lt(p, q, e)
133	
134	def lt_succ_le_succ(+a: Nat, +b: Nat, e: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_le(1n+a, b) == True{} : Bool}:
135	  match a b:
136	    case _ 0n:
137	      Empty.absurd({Nat.is_le(1n+a, 0n) == True{} : Bool}, lt_zero_absurd(a, e))
138	    case 0n 1n+q:
139	      zero_le(q)
140	    case 1n+p 1n+q:
141	      lt_succ_le_succ(p, q, e)
142	
143	def le_trans(+a: Nat, +b: Nat, +c: Nat, ab: {Nat.is_le(a, b) == True{} : Bool}, bc: {Nat.is_le(b, c) == True{} : Bool}) -> {Nat.is_le(a, c) == True{} : Bool}:
144	  match a b c:
145	    case 0n _ _:
146	      zero_le(c)
147	    case 1n+p 0n _:
148	      Empty.absurd({Nat.is_le(1n+p, c) == True{} : Bool}, L.false_true(ab))
149	    case 1n+p 1n+q 0n:
150	      Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, L.false_true(bc))
151	    case 1n+p 1n+q 1n+r:
152	      le_trans(p, q, r, ab, bc)
153	
154	def lt_le_trans(+a: Nat, +b: Nat, +c: Nat, ab: {Nat.is_lt(a, b) == True{} : Bool}, bc: {Nat.is_le(b, c) == True{} : Bool}) -> {Nat.is_lt(a, c) == True{} : Bool}:
155	  succ_le_lt(a, c, le_trans(1n+a, b, c, lt_succ_le_succ(a, b, ab), bc))
156	
157	def le_lt_trans(+a: Nat, +b: Nat, +c: Nat, ab: {Nat.is_le(a, b) == True{} : Bool}, bc: {Nat.is_lt(b, c) == True{} : Bool}) -> {Nat.is_lt(a, c) == True{} : Bool}:
158	  succ_le_lt(a, c, le_trans(1n+a, 1n+b, c, ab, lt_succ_le_succ(b, c, bc)))
159	
160	def lt_trans(+a: Nat, +b: Nat, +c: Nat, ab: {Nat.is_lt(a, b) == True{} : Bool}, bc: {Nat.is_lt(b, c) == True{} : Bool}) -> {Nat.is_lt(a, c) == True{} : Bool}:
161	  lt_le_trans(a, b, c, ab, lt_le(b, c, bc))
162	
163	# is_lt(a, b) == False gives b <= a.
164	def not_lt_le(+a: Nat, +b: Nat, e: {Nat.is_lt(a, b) == False{} : Bool}) -> {Nat.is_le(b, a) == True{} : Bool}:
165	  match a b:
166	    case _ 0n:
167	      zero_le(a)
168	    case 0n 1n+q:
169	      Empty.absurd({Nat.is_le(1n+q, 0n) == True{} : Bool}, L.true_false(e))
170	    case 1n+p 1n+q:
171	      not_lt_le(p, q, e)
172	
173	def le_not_lt(+a: Nat, +b: Nat, e: {Nat.is_le(b, a) == True{} : Bool}) -> {Nat.is_lt(a, b) == False{} : Bool}:
174	  match a b:
175	    case _ 0n:
176	      not_lt_zero(a)
177	    case 0n 1n+q:
178	      Empty.absurd({Nat.is_lt(0n, 1n+q) == False{} : Bool}, L.false_true(e))
179	    case 1n+p 1n+q:
180	      le_not_lt(p, q, e)
181	
182	def lt_not_le(+a: Nat, +b: Nat, e: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_le(b, a) == False{} : Bool}:
183	  match a b:
184	    case _ 0n:
185	      Empty.absurd({Nat.is_le(0n, a) == False{} : Bool}, lt_zero_absurd(a, e))
186	    case 0n 1n+q:
187	      {==}
188	    case 1n+p 1n+q:
189	      lt_not_le(p, q, e)
190	
191	def not_le_lt(+a: Nat, +b: Nat, e: {Nat.is_le(a, b) == False{} : Bool}) -> {Nat.is_lt(b, a) == True{} : Bool}:
192	  match a b:
193	    case 0n 0n:
194	      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, L.true_false(e))
195	    case 0n 1n+q:
196	      Empty.absurd({Nat.is_lt(1n+q, 0n) == True{} : Bool}, L.true_false(e))
197	    case 1n+p 0n:
198	      {==}
199	    case 1n+p 1n+q:
200	      not_le_lt(p, q, e)
201	
202	def lt_asym(+a: Nat, +b: Nat, ab: {Nat.is_lt(a, b) == True{} : Bool}, ba: {Nat.is_lt(b, a) == True{} : Bool}) -> Empty:
203	  L.true_not_false(Nat.is_lt(a, a), lt_trans(a, b, a, ab, ba), lt_irrefl(a))
204	
205	def le_antisym(+a: Nat, +b: Nat, ab: {Nat.is_le(a, b) == True{} : Bool}, ba: {Nat.is_le(b, a) == True{} : Bool}) -> {a == b : Nat}:
206	  match a b:
207	    case 0n 0n:
208	      {==}
209	    case 0n 1n+q:
210	      Empty.absurd({0n == 1n+q : Nat}, L.false_true(ba))
211	    case 1n+p 0n:
212	      Empty.absurd({1n+p == 0n : Nat}, L.false_true(ab))
213	    case 1n+p 1n+q:
214	      succ_cong(p, q, le_antisym(p, q, ab, ba))
215	
216	def eq_le(+a: Nat, +b: Nat, e: {a == b : Nat}) -> {Nat.is_le(a, b) == True{} : Bool}:
217	  %e : {Nat.is_le(a, _) == True{} : Bool}
218	  le_refl(a)
219	
220	def lt_ne(+a: Nat, +b: Nat, lt: {Nat.is_lt(a, b) == True{} : Bool}, e: {a == b : Nat}) -> Empty:
221	  L.true_not_false(Nat.is_lt(a, a), Equal.trans(Bool, Nat.is_lt(a, a), Nat.is_lt(a, b), True{}, Equal.cong(Nat, Bool, x => Nat.is_lt(a, x), a, b, e), lt), lt_irrefl(a))
222	
223	def eq_from_is_eq(+a: Nat, +b: Nat, e: {Nat.is_eq(a, b) == True{} : Bool}) -> {a == b : Nat}:
224	  match a b:
225	    case 0n 0n:
226	      {==}
227	    case 0n 1n+q:
228	      Empty.absurd({0n == 1n+q : Nat}, L.false_true(e))
229	    case 1n+p 0n:
230	      Empty.absurd({1n+p == 0n : Nat}, L.false_true(e))
231	    case 1n+p 1n+q:
232	      succ_cong(p, q, eq_from_is_eq(p, q, e))
233	
234	def is_eq_refl(+a: Nat) -> {Nat.is_eq(a, a) == True{} : Bool}:
235	  match a:
236	    case 0n:
237	      {==}
238	    case 1n+p:
239	      is_eq_refl(p)
240	
241	def is_eq_lt(+a: Nat, +b: Nat, e: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_eq(a, b) == False{} : Bool}:
242	  match a b:
243	    case _ 0n:
244	      Empty.absurd({Nat.is_eq(a, 0n) == False{} : Bool}, lt_zero_absurd(a, e))
245	    case 0n 1n+q:
246	      {==}
247	    case 1n+p 1n+q:
248	      is_eq_lt(p, q, e)
249	
250	def lt_or_eq(+a: Nat, +b: Nat, e: {Nat.is_le(a, b) == True{} : Bool}, ne: {Nat.is_eq(a, b) == False{} : Bool}) -> {Nat.is_lt(a, b) == True{} : Bool}:
251	  match a b:
252	    case 0n 0n:
253	      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, L.true_false(ne))
254	    case 0n 1n+q:
255	      {==}
256	    case 1n+p 0n:
257	      Empty.absurd({Nat.is_lt(1n+p, 0n) == True{} : Bool}, L.false_true(e))
258	    case 1n+p 1n+q:
259	      lt_or_eq(p, q, e, ne)
260	
261	# ---- addition and subtraction ----
262	
263	def add_sub_cancel(+a: Nat, +b: Nat) -> {Nat.sub(Nat.add(a, b), a) == b : Nat}:
264	  match a b:
265	    case 0n 0n:
266	      {==}
267	    case 0n 1n+q:
268	      {==}
269	    case 1n+p _:
270	      add_sub_cancel(p, b)
271	
272	def sub_add(+a: Nat, +b: Nat, e: {Nat.is_le(b, a) == True{} : Bool}) -> {Nat.add(b, Nat.sub(a, b)) == a : Nat}:
273	  match a b:
274	    case 0n 0n:
275	      {==}
276	    case 1n+p 0n:
277	      {==}
278	    case 0n 1n+q:
279	      Empty.absurd({Nat.add(1n+q, Nat.sub(0n, 1n+q)) == 0n : Nat}, L.false_true(e))
280	    case 1n+p 1n+q:
281	      succ_cong(Nat.add(q, Nat.sub(p, q)), p, sub_add(p, q, e))
282	
283	def sub_zero(+n: Nat) -> {Nat.sub(n, 0n) == n : Nat}:
284	  match n:
285	    case 0n:
286	      {==}
287	    case 1n+p:
288	      {==}
289	
290	def sub_self(+n: Nat) -> {Nat.sub(n, n) == 0n : Nat}:
291	  match n:
292	    case 0n:
293	      {==}
294	    case 1n+p:
295	      sub_self(p)
296	
297	def sub_succ_left(+a: Nat, +b: Nat, e: {Nat.is_le(b, a) == True{} : Bool}) -> {Nat.sub(1n+a, b) == 1n+Nat.sub(a, b) : Nat}:
298	  match a b:
299	    case _ 0n:
300	      %Equal.sym(Nat, Nat.sub(a, 0n), a, sub_zero(a)) : {1n+a == 1n+_ : Nat}
301	      {==}
302	    case 0n 1n+q:
303	      Empty.absurd({Nat.sub(1n, 1n+q) == 1n+Nat.sub(0n, 1n+q) : Nat}, L.false_true(e))
304	    case 1n+p 1n+q:
305	      sub_succ_left(p, q, e)
306	
307	def sub_lt(+a: Nat, +b: Nat, +c: Nat, le: {Nat.is_le(b, a) == True{} : Bool}, lt: {Nat.is_lt(a, Nat.add(b, c)) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(a, b), c) == True{} : Bool}:
308	  match a b:
309	    case _ 0n:
310	      %Equal.sym(Nat, Nat.sub(a, 0n), a, sub_zero(a)) : {Nat.is_lt(_, c) == True{} : Bool}
311	      lt
312	    case 0n 1n+q:
313	      Empty.absurd({Nat.is_lt(Nat.sub(0n, 1n+q), c) == True{} : Bool}, L.false_true(le))
314	    case 1n+p 1n+q:
315	      sub_lt(p, q, c, le, lt)
316	
317	def le_add_right(+a: Nat, +b: Nat) -> {Nat.is_le(a, Nat.add(a, b)) == True{} : Bool}:
318	  match a:
319	    case 0n:
320	      zero_le(b)
321	    case 1n+p:
322	      le_add_right(p, b)
323	
324	def lt_add_left(+a: Nat, +b: Nat, +c: Nat, e: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_lt(Nat.add(c, a), Nat.add(c, b)) == True{} : Bool}:
325	  match c:
326	    case 0n:
327	      e
328	    case 1n+r:
329	      lt_add_left(a, b, r, e)
330	
331	def le_add_left(+a: Nat, +b: Nat, +c: Nat, e: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(Nat.add(c, a), Nat.add(c, b)) == True{} : Bool}:
332	  match c:
333	    case 0n:
334	      e
335	    case 1n+r:
336	      le_add_left(a, b, r, e)
337	
338	# ---- doubling and powers of two (spec/common.bend pow2) ----
339	
340	def double_inj(+a: Nat, +b: Nat, e: {Nat.double(a) == Nat.double(b) : Nat}) -> {a == b : Nat}:
341	  match a b:
342	    case 0n 0n:
343	      {==}
344	    case 0n 1n+q:
345	      Empty.absurd({0n == 1n+q : Nat}, zero_succ(1n+Nat.double(q), e))
346	    case 1n+p 0n:
347	      Empty.absurd({1n+p == 0n : Nat}, succ_zero(1n+Nat.double(p), e))
348	    case 1n+p 1n+q:
349	      succ_cong(p, q, double_inj(p, q, succ_inj(Nat.double(p), Nat.double(q), succ_inj(1n+Nat.double(p), 1n+Nat.double(q), e))))
350	
351	def even_odd(+a: Nat, +b: Nat, e: {Nat.double(a) == 1n+Nat.double(b) : Nat}) -> Empty:
352	  match a b:
353	    case 0n _:
354	      zero_succ(Nat.double(b), e)
355	    case 1n+p 0n:
356	      succ_zero(Nat.double(p), succ_inj(1n+Nat.double(p), 0n, e))
357	    case 1n+p 1n+q:
358	      even_odd(p, q, succ_inj(Nat.double(p), 1n+Nat.double(q), succ_inj(1n+Nat.double(p), 2n+Nat.double(q), e)))
359	
360	# bit + 2u == bit' + 2v determines both parts.
361	def bit_split_bit(+b: Bool, +c: Bool, +u: Nat, +v: Nat, e: {Nat.add(S.bit_value(b), Nat.double(u)) == Nat.add(S.bit_value(c), Nat.double(v)) : Nat}) -> {b == c : Bool}:
362	  match b c:
363	    case False{} False{}:
364	      {==}
365	    case True{} True{}:
366	      {==}
367	    case False{} True{}:
368	      Empty.absurd({False{} == True{} : Bool}, even_odd(u, v, e))
369	    case True{} False{}:
370	      Empty.absurd({True{} == False{} : Bool}, even_odd(v, u, Equal.sym(Nat, 1n+Nat.double(u), Nat.double(v), e)))
371	
372	def bit_split_val(+b: Bool, +c: Bool, +u: Nat, +v: Nat, e: {Nat.add(S.bit_value(b), Nat.double(u)) == Nat.add(S.bit_value(c), Nat.double(v)) : Nat}) -> {u == v : Nat}:
373	  match b c:
374	    case False{} False{}:
375	      double_inj(u, v, e)
376	    case True{} True{}:
377	      double_inj(u, v, succ_inj(Nat.double(u), Nat.double(v), e))
378	    case False{} True{}:
379	      Empty.absurd({u == v : Nat}, even_odd(u, v, e))
380	    case True{} False{}:
381	      Empty.absurd({u == v : Nat}, even_odd(v, u, Equal.sym(Nat, 1n+Nat.double(u), Nat.double(v), e)))
382	
383	def double_lt(+a: Nat, +b: Nat, e: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_lt(Nat.double(a), Nat.double(b)) == True{} : Bool}:
384	  match a b:
385	    case _ 0n:
386	      Empty.absurd({Nat.is_lt(Nat.double(a), 0n) == True{} : Bool}, lt_zero_absurd(a, e))
387	    case 0n 1n+q:
388	      {==}
389	    case 1n+p 1n+q:
390	      double_lt(p, q, e)
391	
392	def double_le(+a: Nat, +b: Nat, e: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(Nat.double(a), Nat.double(b)) == True{} : Bool}:
393	  match a b:
394	    case 0n _:
395	      zero_le(Nat.double(b))
396	    case 1n+p 0n:
397	      Empty.absurd({Nat.is_le(Nat.double(1n+p), 0n) == True{} : Bool}, L.false_true(e))
398	    case 1n+p 1n+q:
399	      double_le(p, q, e)
400	
401	# bit + 2u < 2v gives u < v.
402	def bit_double_lt(+b: Bool, +u: Nat, +v: Nat, e: {Nat.is_lt(Nat.add(S.bit_value(b), Nat.double(u)), Nat.double(v)) == True{} : Bool}) -> {Nat.is_lt(u, v) == True{} : Bool}:
403	  match b u v:
404	    case _ _ 0n:
405	      Empty.absurd({Nat.is_lt(u, 0n) == True{} : Bool}, lt_zero_absurd(Nat.add(S.bit_value(b), Nat.double(u)), e))
406	    case _ 0n 1n+q:
407	      {==}
408	    case False{} 1n+p 1n+q:
409	      bit_double_lt(False{}, p, q, e)
410	    case True{} 1n+p 1n+q:
411	      bit_double_lt(True{}, p, q, e)
412	
413	def double_lt_bit(+b: Bool, +u: Nat, +v: Nat, e: {Nat.is_lt(u, v) == True{} : Bool}) -> {Nat.is_lt(Nat.add(S.bit_value(b), Nat.double(u)), Nat.double(v)) == True{} : Bool}:
414	  match b u v:
415	    case _ _ 0n:
416	      Empty.absurd({Nat.is_lt(Nat.add(S.bit_value(b), Nat.double(u)), 0n) == True{} : Bool}, lt_zero_absurd(u, e))
417	    case False{} 0n 1n+q:
418	      {==}
419	    case True{} 0n 1n+q:
420	      {==}
421	    case False{} 1n+p 1n+q:
422	      double_lt_bit(False{}, p, q, e)
423	    case True{} 1n+p 1n+q:
424	      double_lt_bit(True{}, p, q, e)
425	
426	def double_self_le(+n: Nat) -> {Nat.is_le(n, Nat.double(n)) == True{} : Bool}:
427	  match n:
428	    case 0n:
429	      {==}
430	    case 1n+p:
431	      le_trans(p, Nat.double(p), 1n+Nat.double(p), double_self_le(p), le_succ(Nat.double(p)))
432	
433	def double_succ_le(+n: Nat, e: {Nat.is_le(1n, n) == True{} : Bool}) -> {Nat.is_le(1n+n, Nat.double(n)) == True{} : Bool}:
434	  match n:
435	    case 0n:
436	      Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, L.false_true(e))
437	    case 1n+p:
438	      double_self_le(p)
439	
440	def pow2_pos(+k: Nat) -> {Nat.is_le(1n, SC.pow2(k)) == True{} : Bool}:
441	  match k:
442	    case 0n:
443	      {==}
444	    case 1n+p:
445	      le_trans(1n, SC.pow2(p), Nat.double(SC.pow2(p)), pow2_pos(p), double_self_le(SC.pow2(p)))
446	
447	def pow2_lt_succ(+k: Nat) -> {Nat.is_lt(SC.pow2(k), SC.pow2(1n+k)) == True{} : Bool}:
448	  succ_le_lt(SC.pow2(k), Nat.double(SC.pow2(k)), double_succ_le(SC.pow2(k), pow2_pos(k)))
449	
450	# 1 <= n gives 1 + n <= 2n.
451	def pow2_mono(+a: Nat, +b: Nat, e: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(SC.pow2(a), SC.pow2(b)) == True{} : Bool}:
452	  match a b:
453	    case 0n _:
454	      pow2_pos(b)
455	    case 1n+p 0n:
456	      Empty.absurd({Nat.is_le(SC.pow2(1n+p), 1n) == True{} : Bool}, L.false_true(e))
457	    case 1n+p 1n+q:
458	      double_le(SC.pow2(p), SC.pow2(q), pow2_mono(p, q, e))
459	
460	def pow2_strict(+a: Nat, +b: Nat, e: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_lt(SC.pow2(a), SC.pow2(b)) == True{} : Bool}:
461	  match b:
462	    case 0n:
463	      Empty.absurd({Nat.is_lt(SC.pow2(a), 1n) == True{} : Bool}, lt_zero_absurd(a, e))
464	    case 1n+q:
465	      lt_le_trans(SC.pow2(a), SC.pow2(1n+a), SC.pow2(1n+q), pow2_lt_succ(a), pow2_mono(1n+a, 1n+q, lt_succ_le_succ(a, 1n+q, e)))
466	
467	# pred(2v) == 1 + 2 pred(v) for v >= 1.
468	def pred_double(+v: Nat, e: {Nat.is_le(1n, v) == True{} : Bool}) -> {Nat.sub(Nat.double(v), 1n) == 1n+Nat.double(Nat.sub(v, 1n)) : Nat}:
469	  match v:
470	    case 0n:
471	      Empty.absurd({Nat.sub(0n, 1n) == 1n+Nat.double(Nat.sub(0n, 1n)) : Nat}, L.false_true(e))
472	    case 1n+p:
473	      %Equal.sym(Nat, Nat.sub(p, 0n), p, sub_zero(p)) : {1n+Nat.double(p) == 1n+Nat.double(_) : Nat}
474	      {==}
475	
476	def add_double(+a: Nat, +b: Nat) -> {Nat.add(Nat.double(a), Nat.double(b)) == Nat.double(Nat.add(a, b)) : Nat}:
477	  match a:
478	    case 0n:
479	      {==}
480	    case 1n+p:
481	      succ_cong(1n+Nat.add(Nat.double(p), Nat.double(b)), 1n+Nat.double(Nat.add(p, b)), succ_cong(Nat.add(Nat.double(p), Nat.double(b)), Nat.double(Nat.add(p, b)), add_double(p, b)))
482	
483	# ---- halving ----
484	#
485	# `Nat.div(n, 2n)` is what the flat-array walks use to step from a block's
486	# half size to the next one (the C references use `h >> 1`). Both facts below
487	# come from Base's own `Nat.divmod.go`, which recurses structurally on the
488	# dividend, so two unfoldings of `Nat.add(2n, i)` are a definitional step.
489	
490	def bump2(p: Nat & Nat) -> Nat & Nat:
491	  (q, r) = p
492	  (1n+q, r)
493	
494	def acc2(i: Nat, m: Nat, +d: Nat, +r: Nat) -> {Nat.divmod.go(i, m, 1n+d, r) == bump2(Nat.divmod.go(i, m, d, r)) : Nat & Nat}:
495	  match i m:
496	    case 0n _:
497	      {==}
498	    case 1n+np 0n:
499	      acc2(np, r, 1n+d, 0n)
500	    case 1n+np 1n+mp:
501	      acc2(np, mp, d, 1n+r)
502	
503	def peel2(+i: Nat, +d: Nat) -> {Nat.divmod.go(Nat.add(2n, i), 1n, d, 0n) == Nat.divmod.go(i, 1n, 1n+d, 0n) : Nat & Nat}:
504	  {==}
505	
506	def fst_bump2(p: Nat & Nat) -> {Pair.fst(Nat, Nat, bump2(p)) == 1n+Pair.fst(Nat, Nat, p) : Nat}:
507	  (q, r) = p
508	  {==}
509	
510	def div2_step(+i: Nat) -> {Nat.div(Nat.add(2n, i), 2n) == 1n+Nat.div(i, 2n) : Nat}:
511	  Equal.trans(Nat, Pair.fst(Nat, Nat, Nat.divmod.go(Nat.add(2n, i), 1n, 0n, 0n)), Pair.fst(Nat, Nat, bump2(Nat.divmod.go(i, 1n, 0n, 0n))), 1n+Pair.fst(Nat, Nat, Nat.divmod.go(i, 1n, 0n, 0n)),
512	    Equal.cong(Nat & Nat, Nat, pq => Pair.fst(Nat, Nat, pq), Nat.divmod.go(Nat.add(2n, i), 1n, 0n, 0n), bump2(Nat.divmod.go(i, 1n, 0n, 0n)),
513	      Equal.trans(Nat & Nat, Nat.divmod.go(Nat.add(2n, i), 1n, 0n, 0n), Nat.divmod.go(i, 1n, 1n, 0n), bump2(Nat.divmod.go(i, 1n, 0n, 0n)),
514	        peel2(i, 0n), acc2(i, 1n, 0n, 0n))),
515	    fst_bump2(Nat.divmod.go(i, 1n, 0n, 0n)))
516	
517	def double_succ(+y: Nat) -> {Nat.double(1n+y) == Nat.add(2n, Nat.double(y)) : Nat}:
518	  %Equal.sym(Nat, Nat.double(y), Nat.add(y, y), NA.double_self(y)) : {Nat.double(1n+y) == Nat.add(2n, _) : Nat}
519	  %Equal.sym(Nat, Nat.double(1n+y), Nat.add(1n+y, 1n+y), NA.double_self(1n+y)) : {_ == Nat.add(2n, Nat.add(y, y)) : Nat}
520	  succ_cong(Nat.add(y, 1n+y), 1n+Nat.add(y, y), add_succ(y, y))
521	
522	def div2_double(x: Nat) -> {Nat.div(Nat.double(x), 2n) == x : Nat}:
523	  match x:
524	    case 0n:
525	      {==}
526	    case 1n+ +y:
527	      %double_succ(y) : {Nat.div(_, 2n) == 1n+y : Nat}
528	      %Equal.sym(Nat, Nat.div(Nat.add(2n, Nat.double(y)), 2n), 1n+Nat.div(Nat.double(y), 2n), div2_step(Nat.double(y))) : {_ == 1n+y : Nat}
529	      succ_cong(Nat.div(Nat.double(y), 2n), y, div2_double(y))
530	
531	# 2^(1+r) / 2 = 2^r
532	def div2_pow2(+r: Nat) -> {Nat.div(SC.pow2(1n+r), 2n) == SC.pow2(r) : Nat}:
533	  div2_double(SC.pow2(r))
534	
535	def min_left(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.min(a, b) == a : Nat}:
536	  match a b:
537	    case 0n _:
538	      {==}
539	    case 1n+ap 0n:
540	      Empty.absurd({Nat.min(1n+ap, 0n) == 1n+ap : Nat}, lt_zero_absurd(1n+ap, h))
541	    case 1n+ap 1n+bp:
542	      succ_cong(Nat.min(ap, bp), ap, min_left(ap, bp, h))
543	
544	def min_right(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == False{} : Bool}) -> {Nat.min(a, b) == b : Nat}:
545	  match a b:
546	    case 0n 0n:
547	      {==}
548	    case 0n 1n+bp:
549	      Empty.absurd({Nat.min(0n, 1n+bp) == 1n+bp : Nat}, zero_succ(0n, Equal.sym(Nat, 1n, 0n, Equal.cong(Bool, Nat, c => S.bit_value(c), True{}, False{}, h))))
550	    case 1n+ap 0n:
551	      {==}
552	    case 1n+ap 1n+bp:
553	      succ_cong(Nat.min(ap, bp), bp, min_right(ap, bp, h))
554	
555	def is_eq_sym_false(+a: Nat, +b: Nat, +h: {Nat.is_eq(a, b) == False{} : Bool}) -> {Nat.is_eq(b, a) == False{} : Bool}:
556	  match a b:
557	    case 0n 0n:
558	      h
559	    case 0n 1n+q:
560	      {==}
561	    case 1n+p 0n:
562	      {==}
563	    case 1n+p 1n+q:
564	      is_eq_sym_false(p, q, h)
565	
566	# a < b  ==>  a + c < b + c
567	def lt_add_r2(+a: Nat, +b: Nat, +c: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_lt(Nat.add(a, c), Nat.add(b, c)) == True{} : Bool}:
568	  match a b:
569	    case 0n 0n:
570	      Empty.absurd({Nat.is_lt(Nat.add(0n, c), Nat.add(0n, c)) == True{} : Bool}, lt_zero_absurd(0n, h))
571	    case 0n 1n+q:
572	      le_lt_succ(c, Nat.add(q, c), le_trans(c, Nat.add(c, q), Nat.add(q, c), le_add_right(c, q), eq_le(Nat.add(c, q), Nat.add(q, c), add_comm(c, q))))
573	    case 1n+p 0n:
574	      Empty.absurd({Nat.is_lt(Nat.add(1n+p, c), Nat.add(0n, c)) == True{} : Bool}, lt_zero_absurd(1n+p, h))
575	    case 1n+p 1n+q:
576	      lt_add_r2(p, q, c, h)