1	import Base
2	import ./natural_addition.bend as Addition
3	
4	import ./u32_comparison.bend as Comparison
5	import ./nat_to_u32_bounds.bend as Bounds
6	import ./word_encoding.bend as WordEncoding
7	import ./nat_division.bend as Division
8	
9	def not_below(+lower: Nat,+value: Nat,room: {Nat.is_le(lower,value) == True{} : Bool}) -> {Nat.is_lt(value,lower) == False{} : Bool}:
10	  match lower value:
11	    case 0n 0n: {==}
12	    case 0n 1n+value: {==}
13	    case 1n+lower 0n: Empty.absurd({True{} == False{} : Bool},WordEncoding.false_true(room))
14	    case 1n+lower 1n+value: not_below(lower,value,room)
15	
16	def cancel_offset_le(+offset: Nat,+left: Nat,+right: Nat,ordered: {Nat.is_le(Nat.add(offset,left),Nat.add(offset,right)) == True{} : Bool}) ->
17	  {Nat.is_le(left,right) == True{} : Bool}:
18	  match offset:
19	    case 0n: ordered
20	    case 1n+previous: cancel_offset_le(previous,left,right,ordered)
21	
22	def equal_of_is_eq(+left: Nat,+right: Nat,equal: {Nat.is_eq(left,right) == True{} : Bool}) -> {left == right : Nat}:
23	  match left right:
24	    case 0n 0n: {==}
25	    case 0n 1n+rest: Empty.absurd({0n == 1n+rest : Nat},WordEncoding.false_true(equal))
26	    case 1n+rest 0n: Empty.absurd({1n+rest == 0n : Nat},WordEncoding.false_true(equal))
27	    case 1n+ +previous 1n+ +last:
28	      %equal_of_is_eq(previous,last,equal) : {1n+previous == 1n+_ : Nat}
29	      {==}
30	
31	def subtract_zero(+value: Nat) -> {Nat.sub(value,0n) == value : Nat}:
32	  match value:
33	    case 0n: {==}
34	    case 1n+rest: {==}
35	
36	def zero_subtract(value: Nat) -> {Nat.sub(0n,value) == 0n : Nat}:
37	  match value:
38	    case 0n: {==}
39	    case 1n+rest: {==}
40	
41	def subtract_shift(+first: Nat,+row: Nat) -> {Nat.sub(Nat.add(first,row),first) == row : Nat}:
42	  match first:
43	    case 0n: subtract_zero(row)
44	    case 1n+rest: subtract_shift(rest,row)
45	
46	def restore_shift(+first: Nat,+row: Nat,lower: {Nat.is_le(first,row) == True{} : Bool}) -> {Nat.add(first,Nat.sub(row,first)) == row : Nat}:
47	  match first row:
48	    case 0n row: subtract_zero(row)
49	    case 1n+first 0n: Empty.absurd({Nat.add(1n+first,Nat.sub(0n,1n+first)) == 0n : Nat},WordEncoding.false_true(lower))
50	    case 1n+ +first 1n+ +row:
51	      Equal.cong(Nat,Nat,n => 1n+n,Nat.add(first,Nat.sub(row,first)),row,restore_shift(first,row,lower))
52	
53	def cancel_sum(+offset: Nat,+left: Nat,+right: Nat,equation: {Nat.add(offset,left) == Nat.add(offset,right) : Nat}) -> {left == right : Nat}:
54	  Equal.trans(Nat,left,Nat.sub(Nat.add(offset,left),offset),right,Equal.sym(Nat,Nat.sub(Nat.add(offset,left),offset),left,subtract_shift(offset,left)),
55	    Equal.trans(Nat,Nat.sub(Nat.add(offset,left),offset),Nat.sub(Nat.add(offset,right),offset),right,
56	      Equal.cong(Nat,Nat,sum => Nat.sub(sum,offset),Nat.add(offset,left),Nat.add(offset,right),equation),subtract_shift(offset,right)))
57	
58	def positive_difference(+end: Nat,+begin: Nat,positive: {Nat.is_lt(begin,end) == True{} : Bool}) -> {Nat.is_lt(0n,Nat.sub(end,begin)) == True{} : Bool}:
59	  match end begin:
60	    case 0n 0n: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(positive))
61	    case 0n 1n+begin: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(positive))
62	    case 1n+end 0n: {==}
63	    case 1n+end 1n+begin: positive_difference(end,begin,positive)
64	
65	def positive_has_last(+size: Nat,positive: {Nat.is_lt(0n,size) == True{} : Bool}) -> {1n+Nat.sub(size,1n) == size : Nat}:
66	  match size:
67	    case 0n: Empty.absurd({1n == 0n : Nat},WordEncoding.false_true(positive))
68	    case 1n+ +rest:
69	      %subtract_zero(rest) : {1n+Nat.sub(rest,0n) == 1n+_ : Nat}
70	      {==}
71	
72	def split_at_element(+total: Nat,+index: Nat,inside: {Nat.is_lt(index,total) == True{} : Bool}) ->
73	  {Nat.add(index,1n+Nat.sub(total,1n+index)) == total : Nat}:
74	  match total index:
75	    case 0n 0n: Empty.absurd({1n == 0n : Nat},WordEncoding.false_true(inside))
76	    case 1n+ +rest 0n:
77	      Equal.cong(Nat,Nat,n => 1n+n,Nat.sub(rest,0n),rest,subtract_zero(rest))
78	    case 0n 1n+ +index:
79	      Empty.absurd({Nat.add(1n+index,1n) == 0n : Nat},WordEncoding.false_true(inside))
80	    case 1n+ +rest 1n+ +index:
81	      Equal.cong(Nat,Nat,n => 1n+n,Nat.add(index,1n+Nat.sub(rest,1n+index)),rest,split_at_element(rest,index,inside))
82	
83	# No number is below zero.
84	def below_zero(+value: Nat,below: {Nat.is_lt(value,0n) == True{} : Bool}) -> Empty:
85	  match value:
86	    case 0n: WordEncoding.false_true(below)
87	    case 1n+rest: WordEncoding.false_true(below)
88	
89	type UpperBound<-value: Nat,-limit: Nat> is Data:
90	  Before{inside: {Nat.is_lt(value,limit) == True{} : Bool}}
91	  At{equal: {value == limit : Nat}}
92	
93	def lift_upper_bound(+value: Nat,+limit: Nat,bound: UpperBound<value,limit>) -> UpperBound<1n+value,1n+limit>:
94	  match bound:
95	    case Before{inside}: Before{inside}
96	    case At{equal}: At{Equal.cong(Nat,Nat,n => 1n+n,value,limit,equal)}
97	
98	def upper_bound_cases(+value: Nat,+limit: Nat,bounded: {Nat.is_le(value,limit) == True{} : Bool}) -> UpperBound<value,limit>:
99	  match value limit:
100	    case 0n 0n: At{{==}}
101	    case 0n 1n+rest: Before{{==}}
102	    case 1n+rest 0n: Empty.absurd(UpperBound<1n+rest,0n>,WordEncoding.false_true(bounded))
103	    case 1n+ +previous 1n+ +last: lift_upper_bound(previous,last,upper_bound_cases(previous,last,bounded))
104	
105	def comparison_not_less(+comparison: Cmp,h: {Cmp.is_lt(comparison) == False{} : Bool}) -> {Cmp.is_ge(comparison) == True{} : Bool}:
106	  match comparison:
107	    case LT{}:
108	      Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(Equal.sym(Bool,True{},False{},h)))
109	    case EQ{}: {==}
110	    case GT{}: {==}
111	
112	def comparison_less_not_equal(+comparison: Cmp,less: {Cmp.is_lt(comparison) == True{} : Bool}) -> {Cmp.is_eq(comparison) == False{} : Bool}:
113	  match comparison:
114	    case LT{}: {==}
115	    case EQ{}: Empty.absurd({True{} == False{} : Bool},WordEncoding.false_true(less))
116	    case GT{}: Empty.absurd({False{} == False{} : Bool},WordEncoding.false_true(less))
117	
118	def less_not_equal(+left: Nat,+right: Nat,less: {Nat.is_lt(left,right) == True{} : Bool}) -> {Nat.is_eq(left,right) == False{} : Bool}:
119	  comparison_less_not_equal(Nat.cmp(left,right),less)
120	
121	def equal_reflexive(+value: Nat) -> {Nat.is_eq(value,value) == True{} : Bool}:
122	  match value:
123	    case 0n: {==}
124	    case 1n+rest: equal_reflexive(rest)
125	
126	def equal_symmetric(+left: Nat,+right: Nat) -> {Nat.is_eq(left,right) == Nat.is_eq(right,left) : Bool}:
127	  match left right:
128	    case 0n 0n: {==}
129	    case 0n 1n+right: {==}
130	    case 1n+left 0n: {==}
131	    case 1n+left 1n+right: equal_symmetric(left,right)
132	
133	def zero_le(+a: Nat) -> {Nat.is_le(0n,a) == True{} : Bool}:
134	  match a:
135	    case 0n:
136	      {==}
137	    case 1n+p:
138	      {==}
139	
140	def reflexive(+a: Nat) -> {Nat.is_le(a,a) == True{} : Bool}:
141	  match a:
142	    case 0n:
143	      {==}
144	    case 1n+p:
145	      reflexive(p)
146	
147	def offset_le(offset: Nat,+left: Nat,+right: Nat,ordered: {Nat.is_le(left,right) == True{} : Bool}) ->
148	  {Nat.is_le(Nat.add(offset,left),Nat.add(offset,right)) == True{} : Bool}:
149	  match offset:
150	    case 0n: ordered
151	    case 1n+rest: offset_le(rest,left,right,ordered)
152	
153	def offset_lt(+offset: Nat,+left: Nat,+right: Nat,ordered: {Nat.is_lt(left,right) == True{} : Bool}) ->
154	  {Nat.is_lt(Nat.add(offset,left),Nat.add(offset,right)) == True{} : Bool}:
155	  match offset:
156	    case 0n: ordered
157	    case 1n+rest: offset_lt(rest,left,right,ordered)
158	
159	def cancel_offset_lt(+offset: Nat,+left: Nat,+right: Nat,ordered: {Nat.is_lt(Nat.add(offset,left),Nat.add(offset,right)) == True{} : Bool}) ->
160	  {Nat.is_lt(left,right) == True{} : Bool}:
161	  match offset:
162	    case 0n: ordered
163	    case 1n+rest: cancel_offset_lt(rest,left,right,ordered)
164	
165	def successor(+a: Nat,+b: Nat,h: {Nat.is_le(a,b) == True{} : Bool}) -> {Nat.is_le(a,1n+b) == True{} : Bool}:
166	  match a:
167	    case 0n:
168	      {==}
169	    case 1n+ +p:
170	      match b:
171	        case 0n:
172	          Empty.absurd({Nat.is_le(1n+p,1n) == True{} : Bool},WordEncoding.false_true(h))
173	        case 1n+q:
174	          successor(p,q,h)
175	
176	def transitive(+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,
177	    c) == True{} : Bool}:
178	  match a:
179	    case 0n:
180	      zero_le(c)
181	    case 1n+ +p:
182	      match b:
183	        case 0n:
184	          Empty.absurd({Nat.is_le(1n+p,c) == True{} : Bool},WordEncoding.false_true(ab))
185	        case 1n+ +q:
186	          match c:
187	            case 0n:
188	              Empty.absurd({Nat.is_le(1n+p,0n) == True{} : Bool},WordEncoding.false_true(bc))
189	            case 1n+r:
190	              transitive(p,q,r,ab,bc)
191	
192	def le_add(+a: Nat,+b: Nat) -> {Nat.is_le(a,Nat.add(a,b)) == True{} : Bool}:
193	  match a:
194	    case 0n:
195	      zero_le(b)
196	    case 1n+p:
197	      le_add(p,b)
198	
199	def le_double(+a: Nat) -> {Nat.is_le(a,Nat.double(a)) == True{} : Bool}:
200	  %Addition.double(a) : {Nat.is_le(a,_) == True{} : Bool}
201	  le_add(a,a)
202	
203	def double_le(+a: Nat,+b: Nat,ordered: {Nat.is_le(a,b) == True{} : Bool}) -> {Nat.is_le(Nat.double(a),Nat.double(b)) == True{} : Bool}:
204	  match a b:
205	    case 0n b: zero_le(Nat.double(b))
206	    case 1n+a 0n: Empty.absurd({Nat.is_le(Nat.double(1n+a),0n) == True{} : Bool},WordEncoding.false_true(ordered))
207	    case 1n+a 1n+b: double_le(a,b,ordered)
208	
209	def sub_le(+a: Nat,+b: Nat) -> {Nat.is_le(Nat.sub(a,b),a) == True{} : Bool}:
210	  match a b:
211	    case 0n 0n:
212	      {==}
213	    case 0n 1n+b:
214	      {==}
215	    case 1n+ +a 0n:
216	      reflexive(1n+a)
217	    case 1n+ +a 1n+ +b:
218	      successor(Nat.sub(a,b),a,sub_le(a,b))
219	
220	def sub_lt(+a: Nat,+b: Nat,+c: Nat,order: {Nat.is_le(b,a) == True{} : Bool},bound: {Nat.is_lt(a,Nat.add(b,
221	        c)) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(a,b),c) == True{} : Bool}:
222	  match a b:
223	    case 0n 0n:
224	      bound
225	    case 0n 1n+b:
226	      Empty.absurd({Nat.is_lt(0n,c) == True{} : Bool},WordEncoding.false_true(order))
227	    case 1n+a 0n:
228	      bound
229	    case 1n+a 1n+b:
230	      sub_lt(a,b,c,order,bound)
231	
232	def ge_le(+a: Nat,+b: Nat) -> {Nat.is_ge(a,b) == Nat.is_le(b,a) : Bool}:
233	  match a b:
234	    case 0n 0n:
235	      {==}
236	    case 0n 1n+b:
237	      {==}
238	    case 1n+a 0n:
239	      {==}
240	    case 1n+a 1n+b:
241	      ge_le(a,b)
242	
243	def ge_true(+a: Nat,+b: Nat,h: {Nat.is_ge(a,b) == True{} : Bool}) -> {Nat.is_le(b,a) == True{} : Bool}:
244	  %ge_le(a,b) : {_ == True{} : Bool}
245	  h
246	
247	def ge_false(+a: Nat,+b: Nat,h: {Nat.is_ge(a,b) == False{} : Bool}) -> {Nat.is_lt(a,b) == True{} : Bool}:
248	  match a b:
249	    case 0n 0n:
250	      Empty.absurd({Nat.is_lt(0n,0n) == True{} : Bool},WordEncoding.false_true(Equal.sym(Bool,True{},False{},h)))
251	    case 0n 1n+b:
252	      {==}
253	    case 1n+a 0n:
254	      Empty.absurd({Nat.is_lt(1n+a,0n) == True{} : Bool},WordEncoding.false_true(Equal.sym(Bool,True{},False{},h)))
255	    case 1n+a 1n+b:
256	      ge_false(a,b,h)
257	
258	def digit_lt(+a: Nat,+b: Nat,+bit: Bool,h: {Nat.is_lt(a,b) == True{} : Bool}) -> {Nat.is_lt(Comparison.digit(bit,a),
259	    Nat.double(b)) == True{} : Bool}:
260	  match a b bit:
261	    case 0n 0n bit:
262	      Empty.absurd({Nat.is_lt(Comparison.digit(bit,0n),0n) == True{} : Bool},WordEncoding.false_true(h))
263	    case 0n 1n+b False{}:
264	      {==}
265	    case 0n 1n+b True{}:
266	      {==}
267	    case 1n+a 0n bit:
268	      Empty.absurd({Nat.is_lt(Comparison.digit(bit,1n+a),0n) == True{} : Bool},WordEncoding.false_true(h))
269	    case 1n+a 1n+b False{}:
270	      digit_lt(a,b,False{},h)
271	    case 1n+a 1n+b True{}:
272	      digit_lt(a,b,True{},h)
273	
274	def digit_bounded(+a: Nat,+b: Nat,+bit: Bool,+cap: Nat,small: {Nat.is_lt(a,b) == True{} : Bool},large: {Nat.is_le(Nat.double(b),
275	      cap) == True{} : Bool}) -> {Nat.is_le(Comparison.digit(bit,a),cap) == True{} : Bool}:
276	  Bounds.strict_le(Comparison.digit(bit,a),cap,Bounds.nat_trans(Comparison.digit(bit,a),Nat.double(b),cap,digit_lt(a,b,bit,
277	        small),large))
278	
279	def commutative(+a: Nat,+b: Nat) -> {Nat.add(a,b) == Nat.add(b,a) : Nat}:
280	  match a:
281	    case 0n:
282	      Equal.sym(Nat,Nat.add(b,0n),b,Addition.zero_right(b))
283	    case 1n+ +p:
284	      %Equal.sym(Nat,Nat.add(b,1n+p),1n+Nat.add(b,p),Addition.successor_right(b,p)) : {1n+Nat.add(p,b) == _ : Nat}
285	      %commutative(p,b) : {1n+Nat.add(p,b) == 1n+_ : Nat}
286	      {==}
287	
288	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,
289	    c) == True{} : Bool}:
290	  match a b c:
291	    case 0n 0n 0n:
292	      Empty.absurd({Nat.is_lt(0n,0n) == True{} : Bool},WordEncoding.false_true(bc))
293	    case 0n 1n+b 0n:
294	      Empty.absurd({Nat.is_lt(0n,0n) == True{} : Bool},WordEncoding.false_true(bc))
295	    case 0n b 1n+c:
296	      {==}
297	    case 1n+a 0n c:
298	      Empty.absurd({Nat.is_lt(1n+a,c) == True{} : Bool},WordEncoding.false_true(ab))
299	    case 1n+a 1n+b 0n:
300	      Empty.absurd({Nat.is_lt(1n+a,0n) == True{} : Bool},WordEncoding.false_true(bc))
301	    case 1n+a 1n+b 1n+c:
302	      le_lt_trans(a,b,c,ab,bc)
303	
304	def advance_room(+i: Nat,+tail: Nat,+cap: Nat,h: {Nat.is_le(Nat.add(i,1n+tail),cap) == True{} : Bool}) -> {Nat.is_le(Nat.add(1n+i,tail),
305	    cap) == True{} : Bool}:
306	  %Addition.successor_right(i,tail) : {Nat.is_le(_,cap) == True{} : Bool}
307	  h
308	
309	def room_index(+i: Nat,+tail: Nat,+cap: Nat,h: {Nat.is_le(Nat.add(i,1n+tail),cap) == True{} : Bool}) -> {Nat.is_lt(i,cap) == True{} : Bool}:
310	  le_lt_trans(i,Nat.add(i,tail),cap,le_add(i,tail),Bounds.predecessor_strict(Nat.add(i,tail),cap,advance_room(i,tail,cap,h)))
311	
312	# Order structure shared by padding, allocation and mixed-radix indexing.
313	def lt_succ(+a: Nat,+b: Nat,h: {Nat.is_le(a,b) == True{} : Bool}) -> {Nat.is_lt(a,1n+b) == True{} : Bool}:
314	  match a b:
315	    case 0n 0n:
316	      {==}
317	    case 0n 1n+b:
318	      {==}
319	    case 1n+a 0n:
320	      Empty.absurd({Nat.is_lt(1n+a,1n) == True{} : Bool},WordEncoding.false_true(h))
321	    case 1n+a 1n+b:
322	      lt_succ(a,b,h)
323	
324	# Order structure shared by padding, allocation and mixed-radix indexing.
325	def add_le(+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}:
326	  match a b:
327	    case 0n 0n:
328	      reflexive(c)
329	    case 0n 1n+ +b:
330	      successor(c,Nat.add(b,c),
331	        %commutative(c,b) : {Nat.is_le(c,_) == True{} : Bool}
332	        le_add(c,b))
333	    case 1n+a 0n:
334	      Empty.absurd({Nat.is_le(Nat.add(1n+a,c),c) == True{} : Bool},WordEncoding.false_true(h))
335	    case 1n+a 1n+b:
336	      add_le(a,b,c,h)
337	
338	# Order structure shared by padding, allocation and mixed-radix indexing.
339	def add_lt(+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}:
340	  match a b:
341	    case 0n 0n:
342	      Empty.absurd({Nat.is_lt(c,c) == True{} : Bool},WordEncoding.false_true(h))
343	    case 0n 1n+ +b:
344	      lt_succ(c,Nat.add(b,c),
345	        %commutative(c,b) : {Nat.is_le(c,_) == True{} : Bool}
346	        le_add(c,b))
347	    case 1n+a 0n:
348	      Empty.absurd({Nat.is_lt(Nat.add(1n+a,c),c) == True{} : Bool},WordEncoding.false_true(h))
349	    case 1n+a 1n+b:
350	      add_lt(a,b,c,h)
351	
352	# Order structure shared by padding, allocation and mixed-radix indexing.
353	def strict_follow(+a: Nat,+b: Nat,h: {Nat.is_lt(a,b) == True{} : Bool}) -> {Nat.is_le(1n+a,b) == True{} : Bool}:
354	  match a b:
355	    case 0n 0n:
356	      Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(h))
357	    case 0n 1n+b:
358	      zero_le(b)
359	    case 1n+a 0n:
360	      Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(h))
361	    case 1n+a 1n+b:
362	      strict_follow(a,b,h)
363	
364	# Translate a comparison against a remaining extent to its absolute position.
365	def below_difference(+offset: Nat,+value: Nat,+end: Nat,ordered: {Nat.is_le(offset,end) == True{} : Bool}) ->
366	  {Nat.is_lt(value,Nat.sub(end,offset)) == Nat.is_lt(Nat.add(offset,value),end) : Bool}:
367	  match offset end:
368	    case 0n end:
369	      %Equal.sym(Nat,Nat.sub(end,0n),end,subtract_zero(end)) : {Nat.is_lt(value,_) == Nat.is_lt(value,end) : Bool}
370	      {==}
371	    case 1n+offset 0n:
372	      Empty.absurd({Nat.is_lt(value,Nat.sub(0n,1n+offset)) == Nat.is_lt(Nat.add(1n+offset,value),0n) : Bool},WordEncoding.false_true(ordered))
373	    case 1n+offset 1n+end: below_difference(offset,value,end,ordered)
374	
375	# Two opposite bounds identify a natural number.
376	def antisymmetric(+left: Nat,+right: Nat,forward: {Nat.is_le(left,right) == True{} : Bool},backward: {Nat.is_le(right,left) == True{} : Bool}) -> {left == right : Nat}:
377	  match left right:
378	    case 0n 0n: {==}
379	    case 0n 1n+right: Empty.absurd({0n == 1n+right : Nat},WordEncoding.false_true(backward))
380	    case 1n+left 0n: Empty.absurd({1n+left == 0n : Nat},WordEncoding.false_true(forward))
381	    case 1n+ +left 1n+ +right:
382	      Equal.cong(Nat,Nat,value => 1n+value,left,right,antisymmetric(left,right,forward,backward))
383	
384	# Additive complements describe reflected digits without subtraction premises.
385	def below_sum(+value: Nat,+more: Nat) -> {Nat.is_lt(value,Nat.add(value,1n+more)) == True{} : Bool}:
386	  match value:
387	    case 0n: {==}
388	    case 1n+ +rest: below_sum(rest,more)
389	
390	def below_complement(+value: Nat,+more: Nat,+total: Nat,place: {Nat.add(value,1n+more) == total : Nat}) -> {Nat.is_lt(value,total) == True{} : Bool}:
391	  %place : {Nat.is_lt(value,_) == True{} : Bool}
392	  below_sum(value,more)
393	
394	def subtract_one_complement(+left: Nat,+right: Nat) -> {Nat.sub(Nat.add(left,1n+right),1n) == Nat.add(left,right) : Nat}:
395	  Equal.trans(Nat,Nat.sub(Nat.add(left,1n+right),1n),Nat.sub(1n+Nat.add(left,right),1n),Nat.add(left,right),
396	    Equal.cong(Nat,Nat,value => Nat.sub(value,1n),Nat.add(left,1n+right),1n+Nat.add(left,right),Addition.successor_right(left,right)),subtract_zero(Nat.add(left,right)))
397	
398	def reflected_complement(+digit: Nat,+reflected: Nat,+extent: Nat,place: {Nat.add(digit,1n+reflected) == extent : Nat}) ->
399	  {Nat.sub(Nat.sub(extent,1n),digit) == reflected : Nat}:
400	  Equal.trans(Nat,Nat.sub(Nat.sub(extent,1n),digit),Nat.sub(Nat.add(digit,reflected),digit),reflected,
401	    Equal.cong(Nat,Nat,value => Nat.sub(value,digit),Nat.sub(extent,1n),Nat.add(digit,reflected),
402	      Equal.trans(Nat,Nat.sub(extent,1n),Nat.sub(Nat.add(digit,1n+reflected),1n),Nat.add(digit,reflected),
403	        Equal.cong(Nat,Nat,value => Nat.sub(value,1n),extent,Nat.add(digit,1n+reflected),Equal.sym(Nat,Nat.add(digit,1n+reflected),extent,place)),subtract_one_complement(digit,reflected))),subtract_shift(digit,reflected))
404	
405	# Truncated subtraction is adjoint to addition for non-strict bounds.
406	def subtraction_le(+end: Nat,+offset: Nat,+value: Nat) ->
407	  {Nat.is_le(Nat.sub(end,offset),value) == Nat.is_le(end,Nat.add(offset,value)) : Bool}:
408	  match end offset:
409	    case 0n 0n: {==}
410	    case 0n 1n+rest: zero_le(value)
411	    case 1n+rest 0n: {==}
412	    case 1n+rest 1n+offset: subtraction_le(rest,offset,value)
413	
414	# The strict counterpart includes offsets beyond the endpoint.
415	def subtraction_lt(+end: Nat,+offset: Nat,+value: Nat) ->
416	  {Nat.is_lt(value,Nat.sub(end,offset)) == Nat.is_lt(Nat.add(offset,value),end) : Bool}:
417	  match end offset:
418	    case 0n 0n: {==}
419	    case 0n 1n+rest: not_below(0n,value,zero_le(value))
420	    case 1n+rest 0n: {==}
421	    case 1n+rest 1n+offset: subtraction_lt(rest,offset,value)
422	
423	def strict_complement(+left: Nat,+right: Nat) ->
424	  {Nat.is_lt(left,right) == Bool.not(Nat.is_le(right,left)) : Bool}:
425	  match left right:
426	    case 0n 0n: {==}
427	    case 0n 1n+rest: {==}
428	    case 1n+rest 0n: {==}
429	    case 1n+left 1n+right: strict_complement(left,right)
430	
431	def drop_left_le(+offset: Nat,+count: Nat,+stride: Nat,span: {Nat.is_le(Nat.add(offset,count),stride) == True{} : Bool}) ->
432	  {Nat.is_le(count,stride) == True{} : Bool}:
433	  transitive(count,Nat.add(offset,count),stride,
434	    %commutative(count,offset) : {Nat.is_le(count,_) == True{} : Bool}
435	    le_add(count,offset),span)
436	
437	# Adding the window's image-relative start translates a valid padded row.
438	def subtract_from_sum(+offset: Nat,+coordinate: Nat,+padding: Nat,ordered: {Nat.is_le(padding,coordinate) == True{} : Bool}) ->
439	  {Nat.sub(Nat.add(offset,coordinate),padding) == Nat.add(offset,Nat.sub(coordinate,padding)) : Nat}:
440	  match coordinate padding:
441	    case +coordinate 0n: Equal.trans(Nat,Nat.sub(Nat.add(offset,coordinate),0n),Nat.add(offset,coordinate),Nat.add(offset,Nat.sub(coordinate,0n)),subtract_zero(Nat.add(offset,coordinate)),
442	      Equal.cong(Nat,Nat,value => Nat.add(offset,value),coordinate,Nat.sub(coordinate,0n),Equal.sym(Nat,Nat.sub(coordinate,0n),coordinate,subtract_zero(coordinate))))
443	    case 0n 1n+padding: Empty.absurd({Nat.sub(Nat.add(offset,0n),1n+padding) == Nat.add(offset,0n) : Nat},WordEncoding.false_true(ordered))
444	    case 1n+ +coordinate 1n+ +padding:
445	      %Equal.sym(Nat,Nat.add(offset,1n+coordinate),1n+Nat.add(offset,coordinate),Addition.successor_right(offset,coordinate)) :
446	        {Nat.sub(_,1n+padding) == Nat.add(offset,Nat.sub(coordinate,padding)) : Nat}
447	      subtract_from_sum(offset,coordinate,padding,ordered)
448	
449	def le_offset(+offset: Nat,+left: Nat,+right: Nat) -> {Nat.is_le(Nat.add(offset,left),Nat.add(offset,right)) == Nat.is_le(left,right) : Bool}:
450	  match offset:
451	    case 0n: {==}
452	    case 1n+ +rest: le_offset(rest,left,right)
453	
454	def lt_offset(+offset: Nat,+left: Nat,+right: Nat) -> {Nat.is_lt(Nat.add(offset,left),Nat.add(offset,right)) == Nat.is_lt(left,right) : Bool}:
455	  match offset:
456	    case 0n: {==}
457	    case 1n+ +rest: lt_offset(rest,left,right)
458	
459	# A mapped interval remains image-local, including a zero interval at the
460	# next image boundary. This lemma separates row geometry from stored values.
461	def subtract_below(+value: Nat,+amount: Nat,inside: {Nat.is_le(value,amount) == True{} : Bool}) -> {Nat.sub(value,amount) == 0n : Nat}:
462	  match value amount:
463	    case 0n amount: zero_subtract(amount)
464	    case 1n+value 0n: Empty.absurd({Nat.sub(1n+value,0n) == 0n : Nat},WordEncoding.false_true(inside))
465	    case 1n+ +value 1n+ +amount: subtract_below(value,amount,inside)
466	
467	def product_positive(+left: Nat,+right: Nat,left_positive: {Nat.is_lt(0n,left) == True{} : Bool},right_positive: {Nat.is_lt(0n,right) == True{} : Bool}) ->
468	  {Nat.is_lt(0n,Nat.mul(left,right)) == True{} : Bool}:
469	  match left right:
470	    case 0n right: Empty.absurd({Nat.is_lt(0n,Nat.mul(0n,right)) == True{} : Bool},WordEncoding.false_true(left_positive))
471	    case 1n+left 0n: Empty.absurd({Nat.is_lt(0n,Nat.mul(1n+left,0n)) == True{} : Bool},WordEncoding.false_true(right_positive))
472	    case 1n+left 1n+right: {==}
473	
474	def not_less(+left: Nat,+right: Nat,order: {Nat.is_lt(left,right) == False{} : Bool}) -> {Nat.is_le(right,left) == True{} : Bool}:
475	  match left right:
476	    case left 0n: zero_le(left)
477	    case 0n 1n+right: Empty.absurd({Nat.is_le(1n+right,0n) == True{} : Bool},WordEncoding.false_true(Equal.sym(Bool,True{},False{},order)))
478	    case 1n+left 1n+right: not_less(left,right,order)
479	
480	def positive_bound(+value: Nat,+limit: Nat,inside: {Nat.is_lt(value,limit) == True{} : Bool}) -> {Nat.is_lt(0n,limit) == True{} : Bool}:
481	  le_lt_trans(0n,value,limit,zero_le(value),inside)
482	
483	def nonzero_positive(+value: Nat,nonzero: {Nat.is_eq(value,0n) == False{} : Bool}) -> {Nat.is_lt(0n,value) == True{} : Bool}:
484	  match value:
485	    case 0n: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(Equal.sym(Bool,True{},False{},nonzero)))
486	    case 1n+rest: {==}
487	
488	def zero_below(+value: Nat,bounded: {Nat.is_le(value,0n) == True{} : Bool}) -> {value == 0n : Nat}:
489	  match value:
490	    case 0n: {==}
491	    case 1n+rest: Empty.absurd({1n+rest == 0n : Nat},WordEncoding.false_true(bounded))
492	
493	def positive_one(+length: Nat,positive: {Nat.is_lt(0n,length) == True{} : Bool}) -> {Nat.is_le(1n,length) == True{} : Bool}:
494	  strict_follow(0n,length,positive)
495	
496	def last_below(+length: Nat,positive: {Nat.is_lt(0n,length) == True{} : Bool}) ->
497	  {Nat.is_lt(Nat.sub(length,1n),length) == True{} : Bool}:
498	  %positive_has_last(length,positive) : {Nat.is_lt(Nat.sub(length,1n),_) == True{} : Bool}
499	  lt_succ(Nat.sub(length,1n),Nat.sub(length,1n),reflexive(Nat.sub(length,1n)))
500	
501	def twice(+value: Nat) -> {Nat.mul(2n,value) == Nat.add(value,value) : Nat}:
502	  Equal.cong(Nat,Nat,tail => Nat.add(value,tail),Nat.add(value,0n),value,Addition.zero_right(value))
503	
504	def times_one(+value: Nat) -> {Nat.mul(value,1n) == value : Nat}:
505	  match value:
506	    case 0n: {==}
507	    case 1n+ +rest:
508	      Equal.cong(Nat,Nat,value => 1n+value,Nat.mul(rest,1n),rest,times_one(rest))
509	
510	def before_last(+offset: Nat,+length: Nat,inside: {Nat.is_lt(offset,length) == True{} : Bool}) ->
511	  {Nat.is_le(offset,Nat.sub(length,1n)) == True{} : Bool}:
512	  match length:
513	    case 0n:
514	      Empty.absurd({Nat.is_le(offset,0n) == True{} : Bool},WordEncoding.false_true(Equal.trans(Bool,False{},Nat.is_lt(offset,0n),True{},Equal.sym(Bool,Nat.is_lt(offset,0n),False{},Division.lt_zero(offset)),inside)))
515	    case 1n+ +last:
516	      %Equal.sym(Nat,Nat.sub(last,0n),last,subtract_zero(last)) : {Nat.is_le(offset,_) == True{} : Bool}
517	      Division.lt_succ_le(offset,last,inside)
518	
519	def difference_positive(+begin: Nat,+finish: Nat,positive: {Nat.is_lt(0n,Nat.sub(finish,begin)) == True{} : Bool}) ->
520	  {Nat.is_lt(begin,finish) == True{} : Bool}:
521	  match begin finish:
522	    case 0n 0n: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(positive))
523	    case 0n 1n+finish: {==}
524	    case 1n+begin 0n: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(positive))
525	    case 1n+ +begin 1n+ +finish: difference_positive(begin,finish,positive)