1	# Nat order and linear-form lemmas for the OMap weight-balance proofs.
2	import Base
3	import bend-mathlib@0.7.2.0/nat.bend as MNat
4	import bend-mathlib@0.7.2.0/bool.bend as MBool
5	
6	def mul3(+a: Nat) -> Nat:
7	  Nat.mul(3n, a)
8	
9	def wok(+wl: Nat, +wh: Nat) -> Bool:
10	  Bool.and(Nat.is_le(wh, mul3(wl)), Nat.is_le(wl, mul3(wh)))
11	
12	def wok_l(+wl: Nat, +wh: Nat, e: {wok(wl, wh) == True{} : Bool})
13	  -> {Nat.is_le(wh, mul3(wl)) == True{} : Bool}:
14	  MBool.eq_true_of_and_left(Nat.is_le(wh, mul3(wl)), Nat.is_le(wl, mul3(wh)), e)
15	
16	def wok_r(+wl: Nat, +wh: Nat, e: {wok(wl, wh) == True{} : Bool})
17	  -> {Nat.is_le(wl, mul3(wh)) == True{} : Bool}:
18	  MBool.eq_true_of_and_right(Nat.is_le(wh, mul3(wl)), Nat.is_le(wl, mul3(wh)), e)
19	
20	def wok_i(+wl: Nat, +wh: Nat, el: {Nat.is_le(wh, mul3(wl)) == True{} : Bool},
21	  er: {Nat.is_le(wl, mul3(wh)) == True{} : Bool}) -> {wok(wl, wh) == True{} : Bool}:
22	  MBool.and_eq_true(Nat.is_le(wh, mul3(wl)), Nat.is_le(wl, mul3(wh)), el, er)
23	
24	# --- sums ----------------------------------------------------------------------
25	
26	def LE(a: Nat, b: Nat) -> Data:
27	  {Nat.is_le(a, b) == True{} : Bool}
28	
29	def tr(-a: Nat, -b: Nat, -c: Nat, e1: {a == b : Nat}, e2: {b == c : Nat}) -> {a == c : Nat}:
30	  Equal.trans(Nat, a, b, c, e1, e2)
31	
32	def sy(-a: Nat, -b: Nat, e: {a == b : Nat}) -> {b == a : Nat}:
33	  Equal.sym(Nat, a, b, e)
34	
35	def cong_add(-a: Nat, -a2: Nat, -b: Nat, -b2: Nat, e1: {a == a2 : Nat}, e2: {b == b2 : Nat})
36	  -> {Nat.add(a, b) == Nat.add(a2, b2) : Nat}:
37	  %e1 : {Nat.add(a, b) == Nat.add(_, b2) : Nat}
38	  %e2 : {Nat.add(a, b) == Nat.add(a, _) : Nat}
39	  {==}
40	
41	def step(+a: Nat, +b: Nat, +c: Nat, +d: Nat, -x: Nat, -y: Nat, e1: {Nat.add(a, c) == x : Nat},
42	  e2: {Nat.add(b, d) == y : Nat}) -> {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(x, y) : Nat}:
43	  tr(Nat.add(Nat.add(a, b), Nat.add(c, d)), Nat.add(Nat.add(a, c), Nat.add(b, d)), Nat.add(x, y),
44	    MNat.add_add_add_comm(a, b, c, d), cong_add(Nat.add(a, c), x, Nat.add(b, d), y, e1, e2))
45	
46	# --- linear forms c0 + c1*v1 + c2*v2 + c3*v3 + c4*v4 ----------------------------
47	
48	type Lin is Data:
49	  L{c0: Nat, c1: Nat, c2: Nat, c3: Nat, c4: Nat}
50	
51	type Vs is Data:
52	  VS{v1: Nat, v2: Nat, v3: Nat, v4: Nat}
53	
54	def F(p: Lin, v: Vs) -> Nat:
55	  match p v:
56	    case L{c0, c1, c2, c3, c4} VS{+v1, +v2, +v3, +v4}:
57	      Nat.add(c0, Nat.add(Nat.mul(c1, v1), Nat.add(Nat.mul(c2, v2),
58	        Nat.add(Nat.mul(c3, v3), Nat.mul(c4, v4)))))
59	
60	def ladd(p: Lin, q: Lin) -> Lin:
61	  match p q:
62	    case L{a0, a1, a2, a3, a4} L{b0, b1, b2, b3, b4}:
63	      L{Nat.add(a0, b0), Nat.add(a1, b1), Nat.add(a2, b2), Nat.add(a3, b3), Nat.add(a4, b4)}
64	
65	def lsc(k: Nat, +p: Lin) -> Lin:
66	  match k:
67	    case 0n:
68	      L{0n, 0n, 0n, 0n, 0n}
69	    case 1n+j:
70	      ladd(p, lsc(j, p))
71	
72	def lsuc(p: Lin) -> Lin:
73	  match p:
74	    case L{a0, a1, a2, a3, a4}:
75	      L{1n+a0, a1, a2, a3, a4}
76	
77	def lle(p: Lin, q: Lin) -> Bool:
78	  match p q:
79	    case L{a0, a1, a2, a3, a4} L{b0, b1, b2, b3, b4}:
80	      Bool.and(Nat.is_le(a0, b0), Bool.and(Nat.is_le(a1, b1), Bool.and(Nat.is_le(a2, b2),
81	        Bool.and(Nat.is_le(a3, b3), Nat.is_le(a4, b4)))))
82	
83	def F_add(p: Lin, q: Lin, v: Vs) -> {Nat.add(F(p, v), F(q, v)) == F(ladd(p, q), v) : Nat}:
84	  match p q v:
85	    case L{+a0, +a1, +a2, +a3, +a4} L{+b0, +b1, +b2, +b3, +b4} VS{+v1, +v2, +v3, +v4}:
86	      +x1 = Nat.mul(a1, v1)
87	      +x2 = Nat.mul(a2, v2)
88	      +x3 = Nat.mul(a3, v3)
89	      +x4 = Nat.mul(a4, v4)
90	      +y1 = Nat.mul(b1, v1)
91	      +y2 = Nat.mul(b2, v2)
92	      +y3 = Nat.mul(b3, v3)
93	      +y4 = Nat.mul(b4, v4)
94	      +z1 = Nat.mul(Nat.add(a1, b1), v1)
95	      +z2 = Nat.mul(Nat.add(a2, b2), v2)
96	      +z3 = Nat.mul(Nat.add(a3, b3), v3)
97	      +z4 = Nat.mul(Nat.add(a4, b4), v4)
98	      step(a0, Nat.add(x1, Nat.add(x2, Nat.add(x3, x4))), b0, Nat.add(y1, Nat.add(y2, Nat.add(y3, y4))),
99	        Nat.add(a0, b0), Nat.add(z1, Nat.add(z2, Nat.add(z3, z4))), {==},
100	        step(x1, Nat.add(x2, Nat.add(x3, x4)), y1, Nat.add(y2, Nat.add(y3, y4)), z1,
101	          Nat.add(z2, Nat.add(z3, z4)), MNat.add_mul_sym(a1, b1, v1),
102	          step(x2, Nat.add(x3, x4), y2, Nat.add(y3, y4), z2, Nat.add(z3, z4), MNat.add_mul_sym(a2, b2, v2),
103	            step(x3, x4, y3, y4, z3, z4, MNat.add_mul_sym(a3, b3, v3), MNat.add_mul_sym(a4, b4, v4)))))
104	
105	def comb(+p: Lin, +q: Lin, +r: Lin, +s: Lin, +v: Vs, e1: LE(F(p, v), F(q, v)), e2: LE(F(r, v), F(s, v)))
106	  -> LE(F(ladd(p, r), v), F(ladd(q, s), v)):
107	  %F_add(p, r, v) : LE(_, F(ladd(q, s), v))
108	  %F_add(q, s, v) : LE(Nat.add(F(p, v), F(r, v)), _)
109	  MNat.add_le_add(F(p, v), F(r, v), F(q, v), F(s, v), e1, e2)
110	
111	def scale(k: Nat, +p: Lin, +q: Lin, +v: Vs, +e: LE(F(p, v), F(q, v)))
112	  -> LE(F(lsc(k, p), v), F(lsc(k, q), v)):
113	  match k:
114	    case 0n:
115	      MNat.le_refl(F(L{0n, 0n, 0n, 0n, 0n}, v))
116	    case 1n+ +j:
117	      comb(p, q, lsc(j, p), lsc(j, q), v, e, scale(j, p, q, v, e))
118	
119	def and5_1(+a: Bool, +b: Bool, +c: Bool, +d: Bool, +f: Bool,
120	  e: {Bool.and(a, Bool.and(b, Bool.and(c, Bool.and(d, f)))) == True{} : Bool}) -> {a == True{} : Bool}:
121	  MBool.eq_true_of_and_left(a, Bool.and(b, Bool.and(c, Bool.and(d, f))), e)
122	
123	def and5_r(+a: Bool, +b: Bool, +c: Bool, +d: Bool, +f: Bool,
124	  e: {Bool.and(a, Bool.and(b, Bool.and(c, Bool.and(d, f)))) == True{} : Bool})
125	  -> {Bool.and(b, Bool.and(c, Bool.and(d, f))) == True{} : Bool}:
126	  MBool.eq_true_of_and_right(a, Bool.and(b, Bool.and(c, Bool.and(d, f))), e)
127	
128	def F_mono(p: Lin, q: Lin, v: Vs, +h: {lle(p, q) == True{} : Bool}) -> LE(F(p, v), F(q, v)):
129	  match p q v:
130	    case L{+a0, +a1, +a2, +a3, +a4} L{+b0, +b1, +b2, +b3, +b4} VS{+v1, +v2, +v3, +v4}:
131	      +l0 = Nat.is_le(a0, b0)
132	      +l1 = Nat.is_le(a1, b1)
133	      +l2 = Nat.is_le(a2, b2)
134	      +l3 = Nat.is_le(a3, b3)
135	      +l4 = Nat.is_le(a4, b4)
136	      +r1 = and5_r(l0, l1, l2, l3, l4, h)
137	      +r2 = MBool.eq_true_of_and_right(l1, Bool.and(l2, Bool.and(l3, l4)), r1)
138	      +r3 = MBool.eq_true_of_and_right(l2, Bool.and(l3, l4), r2)
139	      +x1 = Nat.mul(a1, v1)
140	      +x2 = Nat.mul(a2, v2)
141	      +x3 = Nat.mul(a3, v3)
142	      +x4 = Nat.mul(a4, v4)
143	      +y1 = Nat.mul(b1, v1)
144	      +y2 = Nat.mul(b2, v2)
145	      +y3 = Nat.mul(b3, v3)
146	      +y4 = Nat.mul(b4, v4)
147	      MNat.add_le_add(a0, Nat.add(x1, Nat.add(x2, Nat.add(x3, x4))), b0, Nat.add(y1, Nat.add(y2, Nat.add(y3, y4))), and5_1(l0, l1, l2, l3, l4, h), MNat.add_le_add(x1, Nat.add(x2, Nat.add(x3, x4)), y1, Nat.add(y2, Nat.add(y3, y4)), MNat.mul_le_mul_right(a1, b1, v1, MBool.eq_true_of_and_left(l1, Bool.and(l2, Bool.and(l3, l4)), r1)), MNat.add_le_add(x2, Nat.add(x3, x4), y2, Nat.add(y3, y4), MNat.mul_le_mul_right(a2, b2, v2, MBool.eq_true_of_and_left(l2, Bool.and(l3, l4), r2)), MNat.add_le_add(x3, x4, y3, y4, MNat.mul_le_mul_right(a3, b3, v3, MBool.eq_true_of_and_left(l3, l4, r3)), MNat.mul_le_mul_right(a4, b4, v4, MBool.eq_true_of_and_right(l3, l4, r3))))))
148	
149	def le_succ_false(x: Nat, e: LE(1n+x, x)) -> Empty:
150	  match x:
151	    case 0n:
152	      MBool.false_ne_true()(e)
153	    case 1n+p:
154	      le_succ_false(p, e)
155	
156	# A combined hypothesis F(p) <= F(q) with q < p term by term is false.
157	def contra(+p: Lin, q: Lin, v: Vs, e: LE(F(p, v), F(q, v)), h: {lle(lsuc(q), p) == True{} : Bool}) -> Empty:
158	  match q v:
159	    case L{+b0, +b1, +b2, +b3, +b4} VS{+v1, +v2, +v3, +v4}:
160	      +vs = {VS{v1, v2, v3, v4} : Vs}
161	      +fq = F(L{b0, b1, b2, b3, b4}, vs)
162	      le_succ_false(fq, MNat.le_trans(1n+fq, F(p, vs), fq, F_mono(L{1n+b0, b1, b2, b3, b4}, p, vs, h), e))
163	
164	# --- from terms to linear forms ------------------------------------------------
165	
166	def F0(v: Vs) -> {F(L{0n, 0n, 0n, 0n, 0n}, v) == 0n : Nat}:
167	  match v:
168	    case VS{v1, v2, v3, v4}:
169	      {==}
170	
171	def cv_c(+n: Nat, v: Vs) -> {n == F(L{n, 0n, 0n, 0n, 0n}, v) : Nat}:
172	  match v:
173	    case VS{v1, v2, v3, v4}:
174	      sy(Nat.add(n, 0n), n, MNat.add_zero(n))
175	
176	def az2(+a: Nat) -> {a == Nat.add(Nat.add(a, 0n), 0n) : Nat}:
177	  sy(Nat.add(Nat.add(a, 0n), 0n), a,
178	    tr(Nat.add(Nat.add(a, 0n), 0n), Nat.add(a, 0n), a, MNat.add_zero(Nat.add(a, 0n)), MNat.add_zero(a)))
179	
180	def cv_1(+a: Nat, +b: Nat, +c: Nat, +d: Nat) -> {a == F(L{0n, 1n, 0n, 0n, 0n}, VS{a, b, c, d}) : Nat}:
181	  az2(a)
182	
183	def cv_2(+a: Nat, +b: Nat, +c: Nat, +d: Nat) -> {b == F(L{0n, 0n, 1n, 0n, 0n}, VS{a, b, c, d}) : Nat}:
184	  az2(b)
185	
186	def cv_3(+a: Nat, +b: Nat, +c: Nat, +d: Nat) -> {c == F(L{0n, 0n, 0n, 1n, 0n}, VS{a, b, c, d}) : Nat}:
187	  az2(c)
188	
189	def cv_4(+a: Nat, +b: Nat, +c: Nat, +d: Nat) -> {d == F(L{0n, 0n, 0n, 0n, 1n}, VS{a, b, c, d}) : Nat}:
190	  sy(Nat.add(d, 0n), d, MNat.add_zero(d))
191	
192	def cv_add(-A: Nat, -B: Nat, +p: Lin, +q: Lin, +v: Vs, eA: {A == F(p, v) : Nat}, eB: {B == F(q, v) : Nat})
193	  -> {Nat.add(A, B) == F(ladd(p, q), v) : Nat}:
194	  tr(Nat.add(A, B), Nat.add(F(p, v), F(q, v)), F(ladd(p, q), v),
195	    cong_add(A, F(p, v), B, F(q, v), eA, eB), F_add(p, q, v))
196	
197	def cv_mul(k: Nat, +A: Nat, +p: Lin, +v: Vs, +eA: {A == F(p, v) : Nat})
198	  -> {Nat.mul(k, A) == F(lsc(k, p), v) : Nat}:
199	  match k:
200	    case 0n:
201	      sy(F(L{0n, 0n, 0n, 0n, 0n}, v), 0n, F0(v))
202	    case 1n+ +j:
203	      cv_add(A, Nat.mul(j, A), p, lsc(j, p), v, eA, cv_mul(j, A, p, v, eA))
204	
205	def cvle(-A: Nat, -B: Nat, -p: Lin, -q: Lin, -v: Vs, eA: {A == F(p, v) : Nat}, eB: {B == F(q, v) : Nat},
206	  h: LE(A, B)) -> LE(F(p, v), F(q, v)):
207	  %eA : LE(_, F(q, v))
208	  %eB : LE(A, _)
209	  h
210	
211	# --- from comparisons to <= ----------------------------------------------------
212	
213	def gt_le(a: Nat, b: Nat, e: {Nat.is_gt(a, b) == True{} : Bool}) -> LE(1n+b, a):
214	  match a b:
215	    case 0n 0n:
216	      Empty.absurd(LE(1n, 0n), MBool.false_ne_true()(e))
217	    case 0n 1n+bp:
218	      Empty.absurd(LE(1n+1n+bp, 0n), MBool.false_ne_true()(e))
219	    case 1n+ap 0n:
220	      MNat.zero_le(ap)
221	    case 1n+ap 1n+bp:
222	      gt_le(ap, bp, e)
223	
224	def ngt_le(a: Nat, b: Nat, e: {Nat.is_gt(a, b) == False{} : Bool}) -> LE(a, b):
225	  match a b:
226	    case 0n b:
227	      MNat.zero_le(b)
228	    case 1n+ap 0n:
229	      Empty.absurd(LE(1n+ap, 0n), MBool.true_ne_false()(e))
230	    case 1n+ap 1n+bp:
231	      ngt_le(ap, bp, e)
232	
233	# Proves x <= y from a refutation of y < x.
234	def by_contra(x: Nat, y: Nat, k: LE(1n+y, x) -> Empty) -> LE(x, y):
235	  match x y:
236	    case 0n y:
237	      MNat.zero_le(y)
238	    case 1n+xp 0n:
239	      Empty.absurd(LE(1n+xp, 0n), k(MNat.zero_le(xp)))
240	    case 1n+xp 1n+yp:
241	      by_contra(xp, yp, k)
242	
243	# --- weight-balance arithmetic -------------------------------------------------
244	# Machine-written certificates. Each lemma refutes its negated goal: it adds the
245	# hypotheses as linear forms, each times a small factor, and contra shows the
246	# sum is false. rls/rld: single/double rotation toward lo; rhs/rhd: toward hi.
247	
248	def alm(+wl: Nat, +wh: Nat) -> Bool:
249	  Bool.and(Nat.is_le(wh, Nat.add(3n, mul3(wl))), Nat.is_le(wl, Nat.add(3n, mul3(wh))))
250	
251	def near(+a: Nat, +b: Nat) -> Bool:
252	  Bool.and(Nat.is_le(a, 1n+b), Nat.is_le(b, 1n+a))
253	
254	def rls.c0a.k(+l: Nat, +a: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, l), a), h4: LE(Nat.add(a, b), Nat.add(3n, Nat.mul(3n, l))), hs: LE(1n+a, Nat.mul(2n, b)), pl: LE(1n, l)) -> Empty:
255	  +v = {VS{l, a, b, 0n} : Vs}
256	  +f_ng = cvle(1n+Nat.mul(3n, l), a, L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v,
257	    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, a, b, 0n))),
258	    cv_2(l, a, b, 0n), ng)
259	  +f_h4 = cvle(Nat.add(a, b), Nat.add(3n, Nat.mul(3n, l)), L{0n, 0n, 1n, 1n, 0n}, L{3n, 3n, 0n, 0n, 0n}, v,
260	    cv_add(a, b, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(l, a, b, 0n), cv_3(l, a, b, 0n)),
261	    cv_add(3n, Nat.mul(3n, l), L{3n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(3n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, a, b, 0n))), h4)
262	  +f_hs = cvle(1n+a, Nat.mul(2n, b), L{1n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 2n, 0n}, v,
263	    cv_add(1n, a, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_c(1n, v), cv_2(l, a, b, 0n)),
264	    cv_mul(2n, b, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(l, a, b, 0n)), hs)
265	  +f_pl = cvle(1n, l, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
266	    cv_c(1n, v),
267	    cv_1(l, a, b, 0n), pl)
268	  contra(L{7n, 9n, 3n, 2n, 0n}, L{6n, 9n, 3n, 2n, 0n}, v,
269	    comb(L{3n, 9n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, L{4n, 0n, 3n, 2n, 0n}, L{6n, 9n, 0n, 2n, 0n}, v, scale(3n, L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, f_ng),
270	    comb(L{0n, 0n, 2n, 2n, 0n}, L{6n, 6n, 0n, 0n, 0n}, L{4n, 0n, 1n, 0n, 0n}, L{0n, 3n, 0n, 2n, 0n}, v, scale(2n, L{0n, 0n, 1n, 1n, 0n}, L{3n, 3n, 0n, 0n, 0n}, v, f_h4),
271	    comb(L{1n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 2n, 0n}, L{3n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, f_hs,
272	    scale(3n, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, f_pl)))), {==})
273	def rls.c0a(+l: Nat, +a: Nat, +b: Nat, h4: LE(Nat.add(a, b), Nat.add(3n, Nat.mul(3n, l))), hs: LE(1n+a, Nat.mul(2n, b)), pl: LE(1n, l)) -> LE(a, Nat.mul(3n, l)):
274	  by_contra(a, Nat.mul(3n, l), ng => rls.c0a.k(l, a, b, ng, h4, hs, pl))
275	
276	def rls.c0b.k(+l: Nat, +a: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, a), l), h2: LE(b, Nat.mul(3n, a)), h3: LE(1n+Nat.mul(3n, l), Nat.add(a, b))) -> Empty:
277	  +v = {VS{l, a, b, 0n} : Vs}
278	  +f_ng = cvle(1n+Nat.mul(3n, a), l, L{1n, 0n, 3n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
279	    cv_add(1n, Nat.mul(3n, a), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, a, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(l, a, b, 0n))),
280	    cv_1(l, a, b, 0n), ng)
281	  +f_h2 = cvle(b, Nat.mul(3n, a), L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v,
282	    cv_3(l, a, b, 0n),
283	    cv_mul(3n, a, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(l, a, b, 0n)), h2)
284	  +f_h3 = cvle(1n+Nat.mul(3n, l), Nat.add(a, b), L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 0n}, v,
285	    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, a, b, 0n))),
286	    cv_add(a, b, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(l, a, b, 0n), cv_3(l, a, b, 0n)), h3)
287	  contra(L{3n, 3n, 6n, 1n, 0n}, L{0n, 2n, 4n, 1n, 0n}, v,
288	    comb(L{2n, 0n, 6n, 0n, 0n}, L{0n, 2n, 0n, 0n, 0n}, L{1n, 3n, 0n, 1n, 0n}, L{0n, 0n, 4n, 1n, 0n}, v, scale(2n, L{1n, 0n, 3n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, f_ng),
289	    comb(L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 3n, 0n, 0n}, L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 0n}, v, f_h2,
290	    f_h3)), {==})
291	def rls.c0b(+l: Nat, +a: Nat, +b: Nat, h2: LE(b, Nat.mul(3n, a)), h3: LE(1n+Nat.mul(3n, l), Nat.add(a, b))) -> LE(l, Nat.mul(3n, a)):
292	  by_contra(l, Nat.mul(3n, a), ng => rls.c0b.k(l, a, b, ng, h2, h3))
293	
294	def rls.w0(+l: Nat, +a: Nat, +b: Nat, +h1: LE(a, Nat.mul(3n, b)), +h2: LE(b, Nat.mul(3n, a)), +h3: LE(1n+Nat.mul(3n, l), Nat.add(a, b)), +h4: LE(Nat.add(a, b), Nat.add(3n, Nat.mul(3n, l))), +hs: LE(1n+a, Nat.mul(2n, b)), +pl: LE(1n, l), +pa: LE(1n, a), +pb: LE(1n, b)) -> {wok(l, a) == True{} : Bool}:
295	  MBool.and_eq_true(Nat.is_le(a, Nat.mul(3n, l)), Nat.is_le(l, Nat.mul(3n, a)), rls.c0a(l, a, b, h4, hs, pl), rls.c0b(l, a, b, h2, h3))
296	
297	def rls.c1a.k(+l: Nat, +a: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, Nat.add(l, a)), b), h2: LE(b, Nat.mul(3n, a))) -> Empty:
298	  +v = {VS{l, a, b, 0n} : Vs}
299	  +f_ng = cvle(1n+Nat.mul(3n, Nat.add(l, a)), b, L{1n, 3n, 3n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v,
300	    cv_add(1n, Nat.mul(3n, Nat.add(l, a)), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 3n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, Nat.add(l, a), L{0n, 1n, 1n, 0n, 0n}, v, cv_add(l, a, L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_1(l, a, b, 0n), cv_2(l, a, b, 0n)))),
301	    cv_3(l, a, b, 0n), ng)
302	  +f_h2 = cvle(b, Nat.mul(3n, a), L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v,
303	    cv_3(l, a, b, 0n),
304	    cv_mul(3n, a, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(l, a, b, 0n)), h2)
305	  contra(L{1n, 3n, 3n, 1n, 0n}, L{0n, 0n, 3n, 1n, 0n}, v,
306	    comb(L{1n, 3n, 3n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v, f_ng,
307	    f_h2), {==})
308	def rls.c1a(+l: Nat, +a: Nat, +b: Nat, h2: LE(b, Nat.mul(3n, a))) -> LE(b, Nat.mul(3n, Nat.add(l, a))):
309	  by_contra(b, Nat.mul(3n, Nat.add(l, a)), ng => rls.c1a.k(l, a, b, ng, h2))
310	
311	def rls.c1b.k(+l: Nat, +a: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, b), Nat.add(l, a)), h3: LE(1n+Nat.mul(3n, l), Nat.add(a, b)), hs: LE(1n+a, Nat.mul(2n, b))) -> Empty:
312	  +v = {VS{l, a, b, 0n} : Vs}
313	  +f_ng = cvle(1n+Nat.mul(3n, b), Nat.add(l, a), L{1n, 0n, 0n, 3n, 0n}, L{0n, 1n, 1n, 0n, 0n}, v,
314	    cv_add(1n, Nat.mul(3n, b), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v, cv_c(1n, v), cv_mul(3n, b, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(l, a, b, 0n))),
315	    cv_add(l, a, L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_1(l, a, b, 0n), cv_2(l, a, b, 0n)), ng)
316	  +f_h3 = cvle(1n+Nat.mul(3n, l), Nat.add(a, b), L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 0n}, v,
317	    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, a, b, 0n))),
318	    cv_add(a, b, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(l, a, b, 0n), cv_3(l, a, b, 0n)), h3)
319	  +f_hs = cvle(1n+a, Nat.mul(2n, b), L{1n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 2n, 0n}, v,
320	    cv_add(1n, a, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_c(1n, v), cv_2(l, a, b, 0n)),
321	    cv_mul(2n, b, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(l, a, b, 0n)), hs)
322	  contra(L{8n, 3n, 4n, 9n, 0n}, L{0n, 3n, 4n, 9n, 0n}, v,
323	    comb(L{3n, 0n, 0n, 9n, 0n}, L{0n, 3n, 3n, 0n, 0n}, L{5n, 3n, 4n, 0n, 0n}, L{0n, 0n, 1n, 9n, 0n}, v, scale(3n, L{1n, 0n, 0n, 3n, 0n}, L{0n, 1n, 1n, 0n, 0n}, v, f_ng),
324	    comb(L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 0n}, L{4n, 0n, 4n, 0n, 0n}, L{0n, 0n, 0n, 8n, 0n}, v, f_h3,
325	    scale(4n, L{1n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 2n, 0n}, v, f_hs))), {==})
326	def rls.c1b(+l: Nat, +a: Nat, +b: Nat, h3: LE(1n+Nat.mul(3n, l), Nat.add(a, b)), hs: LE(1n+a, Nat.mul(2n, b))) -> LE(Nat.add(l, a), Nat.mul(3n, b)):
327	  by_contra(Nat.add(l, a), Nat.mul(3n, b), ng => rls.c1b.k(l, a, b, ng, h3, hs))
328	
329	def rls.w1(+l: Nat, +a: Nat, +b: Nat, +h1: LE(a, Nat.mul(3n, b)), +h2: LE(b, Nat.mul(3n, a)), +h3: LE(1n+Nat.mul(3n, l), Nat.add(a, b)), +h4: LE(Nat.add(a, b), Nat.add(3n, Nat.mul(3n, l))), +hs: LE(1n+a, Nat.mul(2n, b)), +pl: LE(1n, l), +pa: LE(1n, a), +pb: LE(1n, b)) -> {wok(Nat.add(l, a), b) == True{} : Bool}:
330	  MBool.and_eq_true(Nat.is_le(b, Nat.mul(3n, Nat.add(l, a))), Nat.is_le(Nat.add(l, a), Nat.mul(3n, b)), rls.c1a(l, a, b, h2), rls.c1b(l, a, b, h3, hs))
331	
332	def rhs.c0a.k(+l: Nat, +a: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, b), Nat.add(a, l)), h3: LE(1n+Nat.mul(3n, l), Nat.add(b, a)), hs: LE(1n+a, Nat.mul(2n, b))) -> Empty:
333	  +v = {VS{l, a, b, 0n} : Vs}
334	  +f_ng = cvle(1n+Nat.mul(3n, b), Nat.add(a, l), L{1n, 0n, 0n, 3n, 0n}, L{0n, 1n, 1n, 0n, 0n}, v,
335	    cv_add(1n, Nat.mul(3n, b), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v, cv_c(1n, v), cv_mul(3n, b, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(l, a, b, 0n))),
336	    cv_add(a, l, L{0n, 0n, 1n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_2(l, a, b, 0n), cv_1(l, a, b, 0n)), ng)
337	  +f_h3 = cvle(1n+Nat.mul(3n, l), Nat.add(b, a), L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 0n}, v,
338	    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, a, b, 0n))),
339	    cv_add(b, a, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, a, b, 0n), cv_2(l, a, b, 0n)), h3)
340	  +f_hs = cvle(1n+a, Nat.mul(2n, b), L{1n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 2n, 0n}, v,
341	    cv_add(1n, a, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_c(1n, v), cv_2(l, a, b, 0n)),
342	    cv_mul(2n, b, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(l, a, b, 0n)), hs)
343	  contra(L{8n, 3n, 4n, 9n, 0n}, L{0n, 3n, 4n, 9n, 0n}, v,
344	    comb(L{3n, 0n, 0n, 9n, 0n}, L{0n, 3n, 3n, 0n, 0n}, L{5n, 3n, 4n, 0n, 0n}, L{0n, 0n, 1n, 9n, 0n}, v, scale(3n, L{1n, 0n, 0n, 3n, 0n}, L{0n, 1n, 1n, 0n, 0n}, v, f_ng),
345	    comb(L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 0n}, L{4n, 0n, 4n, 0n, 0n}, L{0n, 0n, 0n, 8n, 0n}, v, f_h3,
346	    scale(4n, L{1n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 2n, 0n}, v, f_hs))), {==})
347	def rhs.c0a(+l: Nat, +a: Nat, +b: Nat, h3: LE(1n+Nat.mul(3n, l), Nat.add(b, a)), hs: LE(1n+a, Nat.mul(2n, b))) -> LE(Nat.add(a, l), Nat.mul(3n, b)):
348	  by_contra(Nat.add(a, l), Nat.mul(3n, b), ng => rhs.c0a.k(l, a, b, ng, h3, hs))
349	
350	def rhs.c0b.k(+l: Nat, +a: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, Nat.add(a, l)), b), h2: LE(b, Nat.mul(3n, a))) -> Empty:
351	  +v = {VS{l, a, b, 0n} : Vs}
352	  +f_ng = cvle(1n+Nat.mul(3n, Nat.add(a, l)), b, L{1n, 3n, 3n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v,
353	    cv_add(1n, Nat.mul(3n, Nat.add(a, l)), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 3n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, Nat.add(a, l), L{0n, 1n, 1n, 0n, 0n}, v, cv_add(a, l, L{0n, 0n, 1n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_2(l, a, b, 0n), cv_1(l, a, b, 0n)))),
354	    cv_3(l, a, b, 0n), ng)
355	  +f_h2 = cvle(b, Nat.mul(3n, a), L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v,
356	    cv_3(l, a, b, 0n),
357	    cv_mul(3n, a, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(l, a, b, 0n)), h2)
358	  contra(L{1n, 3n, 3n, 1n, 0n}, L{0n, 0n, 3n, 1n, 0n}, v,
359	    comb(L{1n, 3n, 3n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v, f_ng,
360	    f_h2), {==})
361	def rhs.c0b(+l: Nat, +a: Nat, +b: Nat, h2: LE(b, Nat.mul(3n, a))) -> LE(b, Nat.mul(3n, Nat.add(a, l))):
362	  by_contra(b, Nat.mul(3n, Nat.add(a, l)), ng => rhs.c0b.k(l, a, b, ng, h2))
363	
364	def rhs.w0(+l: Nat, +a: Nat, +b: Nat, +h1: LE(a, Nat.mul(3n, b)), +h2: LE(b, Nat.mul(3n, a)), +h3: LE(1n+Nat.mul(3n, l), Nat.add(b, a)), +h4: LE(Nat.add(b, a), Nat.add(3n, Nat.mul(3n, l))), +hs: LE(1n+a, Nat.mul(2n, b)), +pl: LE(1n, l), +pa: LE(1n, a), +pb: LE(1n, b)) -> {wok(b, Nat.add(a, l)) == True{} : Bool}:
365	  MBool.and_eq_true(Nat.is_le(Nat.add(a, l), Nat.mul(3n, b)), Nat.is_le(b, Nat.mul(3n, Nat.add(a, l))), rhs.c0a(l, a, b, h3, hs), rhs.c0b(l, a, b, h2))
366	
367	def rhs.c1a.k(+l: Nat, +a: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, a), l), h2: LE(b, Nat.mul(3n, a)), h3: LE(1n+Nat.mul(3n, l), Nat.add(b, a))) -> Empty:
368	  +v = {VS{l, a, b, 0n} : Vs}
369	  +f_ng = cvle(1n+Nat.mul(3n, a), l, L{1n, 0n, 3n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
370	    cv_add(1n, Nat.mul(3n, a), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, a, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(l, a, b, 0n))),
371	    cv_1(l, a, b, 0n), ng)
372	  +f_h2 = cvle(b, Nat.mul(3n, a), L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v,
373	    cv_3(l, a, b, 0n),
374	    cv_mul(3n, a, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(l, a, b, 0n)), h2)
375	  +f_h3 = cvle(1n+Nat.mul(3n, l), Nat.add(b, a), L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 0n}, v,
376	    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, a, b, 0n))),
377	    cv_add(b, a, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, a, b, 0n), cv_2(l, a, b, 0n)), h3)
378	  contra(L{3n, 3n, 6n, 1n, 0n}, L{0n, 2n, 4n, 1n, 0n}, v,
379	    comb(L{2n, 0n, 6n, 0n, 0n}, L{0n, 2n, 0n, 0n, 0n}, L{1n, 3n, 0n, 1n, 0n}, L{0n, 0n, 4n, 1n, 0n}, v, scale(2n, L{1n, 0n, 3n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, f_ng),
380	    comb(L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 3n, 0n, 0n}, L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 0n}, v, f_h2,
381	    f_h3)), {==})
382	def rhs.c1a(+l: Nat, +a: Nat, +b: Nat, h2: LE(b, Nat.mul(3n, a)), h3: LE(1n+Nat.mul(3n, l), Nat.add(b, a))) -> LE(l, Nat.mul(3n, a)):
383	  by_contra(l, Nat.mul(3n, a), ng => rhs.c1a.k(l, a, b, ng, h2, h3))
384	
385	def rhs.c1b.k(+l: Nat, +a: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, l), a), h4: LE(Nat.add(b, a), Nat.add(3n, Nat.mul(3n, l))), hs: LE(1n+a, Nat.mul(2n, b)), pl: LE(1n, l)) -> Empty:
386	  +v = {VS{l, a, b, 0n} : Vs}
387	  +f_ng = cvle(1n+Nat.mul(3n, l), a, L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v,
388	    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, a, b, 0n))),
389	    cv_2(l, a, b, 0n), ng)
390	  +f_h4 = cvle(Nat.add(b, a), Nat.add(3n, Nat.mul(3n, l)), L{0n, 0n, 1n, 1n, 0n}, L{3n, 3n, 0n, 0n, 0n}, v,
391	    cv_add(b, a, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, a, b, 0n), cv_2(l, a, b, 0n)),
392	    cv_add(3n, Nat.mul(3n, l), L{3n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(3n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, a, b, 0n))), h4)
393	  +f_hs = cvle(1n+a, Nat.mul(2n, b), L{1n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 2n, 0n}, v,
394	    cv_add(1n, a, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_c(1n, v), cv_2(l, a, b, 0n)),
395	    cv_mul(2n, b, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(l, a, b, 0n)), hs)
396	  +f_pl = cvle(1n, l, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
397	    cv_c(1n, v),
398	    cv_1(l, a, b, 0n), pl)
399	  contra(L{7n, 9n, 3n, 2n, 0n}, L{6n, 9n, 3n, 2n, 0n}, v,
400	    comb(L{3n, 9n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, L{4n, 0n, 3n, 2n, 0n}, L{6n, 9n, 0n, 2n, 0n}, v, scale(3n, L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, f_ng),
401	    comb(L{0n, 0n, 2n, 2n, 0n}, L{6n, 6n, 0n, 0n, 0n}, L{4n, 0n, 1n, 0n, 0n}, L{0n, 3n, 0n, 2n, 0n}, v, scale(2n, L{0n, 0n, 1n, 1n, 0n}, L{3n, 3n, 0n, 0n, 0n}, v, f_h4),
402	    comb(L{1n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 2n, 0n}, L{3n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, f_hs,
403	    scale(3n, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, f_pl)))), {==})
404	def rhs.c1b(+l: Nat, +a: Nat, +b: Nat, h4: LE(Nat.add(b, a), Nat.add(3n, Nat.mul(3n, l))), hs: LE(1n+a, Nat.mul(2n, b)), pl: LE(1n, l)) -> LE(a, Nat.mul(3n, l)):
405	  by_contra(a, Nat.mul(3n, l), ng => rhs.c1b.k(l, a, b, ng, h4, hs, pl))
406	
407	def rhs.w1(+l: Nat, +a: Nat, +b: Nat, +h1: LE(a, Nat.mul(3n, b)), +h2: LE(b, Nat.mul(3n, a)), +h3: LE(1n+Nat.mul(3n, l), Nat.add(b, a)), +h4: LE(Nat.add(b, a), Nat.add(3n, Nat.mul(3n, l))), +hs: LE(1n+a, Nat.mul(2n, b)), +pl: LE(1n, l), +pa: LE(1n, a), +pb: LE(1n, b)) -> {wok(a, l) == True{} : Bool}:
408	  MBool.and_eq_true(Nat.is_le(l, Nat.mul(3n, a)), Nat.is_le(a, Nat.mul(3n, l)), rhs.c1a(l, a, b, h2, h3), rhs.c1b(l, a, b, h4, hs, pl))
409	
410	def rld.c0a.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, Nat.add(l, x)), Nat.add(y, b)), h4: LE(Nat.add(Nat.add(x, y), b), Nat.add(3n, Nat.mul(3n, l))), px: LE(1n, x)) -> Empty:
411	  +v = {VS{l, x, y, b} : Vs}
412	  +f_ng = cvle(1n+Nat.mul(3n, Nat.add(l, x)), Nat.add(y, b), L{1n, 3n, 3n, 0n, 0n}, L{0n, 0n, 0n, 1n, 1n}, v,
413	    cv_add(1n, Nat.mul(3n, Nat.add(l, x)), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 3n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, Nat.add(l, x), L{0n, 1n, 1n, 0n, 0n}, v, cv_add(l, x, L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_1(l, x, y, b), cv_2(l, x, y, b)))),
414	    cv_add(y, b, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 0n, 0n, 1n}, v, cv_3(l, x, y, b), cv_4(l, x, y, b)), ng)
415	  +f_h4 = cvle(Nat.add(Nat.add(x, y), b), Nat.add(3n, Nat.mul(3n, l)), L{0n, 0n, 1n, 1n, 1n}, L{3n, 3n, 0n, 0n, 0n}, v,
416	    cv_add(Nat.add(x, y), b, L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 1n}, v, cv_add(x, y, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(l, x, y, b), cv_3(l, x, y, b)), cv_4(l, x, y, b)),
417	    cv_add(3n, Nat.mul(3n, l), L{3n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(3n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, x, y, b))), h4)
418	  +f_px = cvle(1n, x, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v,
419	    cv_c(1n, v),
420	    cv_2(l, x, y, b), px)
421	  contra(L{4n, 3n, 4n, 1n, 1n}, L{3n, 3n, 3n, 1n, 1n}, v,
422	    comb(L{1n, 3n, 3n, 0n, 0n}, L{0n, 0n, 0n, 1n, 1n}, L{3n, 0n, 1n, 1n, 1n}, L{3n, 3n, 3n, 0n, 0n}, v, f_ng,
423	    comb(L{0n, 0n, 1n, 1n, 1n}, L{3n, 3n, 0n, 0n, 0n}, L{3n, 0n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v, f_h4,
424	    scale(3n, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, f_px))), {==})
425	def rld.c0a(+l: Nat, +x: Nat, +y: Nat, +b: Nat, h4: LE(Nat.add(Nat.add(x, y), b), Nat.add(3n, Nat.mul(3n, l))), px: LE(1n, x)) -> LE(Nat.add(y, b), Nat.mul(3n, Nat.add(l, x))):
426	  by_contra(Nat.add(y, b), Nat.mul(3n, Nat.add(l, x)), ng => rld.c0a.k(l, x, y, b, ng, h4, px))
427	
428	def rld.c0b.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, Nat.add(y, b)), Nat.add(l, x)), h1: LE(Nat.add(x, y), Nat.mul(3n, b)), h3: LE(1n+Nat.mul(3n, l), Nat.add(Nat.add(x, y), b)), h5: LE(x, Nat.mul(3n, y))) -> Empty:
429	  +v = {VS{l, x, y, b} : Vs}
430	  +f_ng = cvle(1n+Nat.mul(3n, Nat.add(y, b)), Nat.add(l, x), L{1n, 0n, 0n, 3n, 3n}, L{0n, 1n, 1n, 0n, 0n}, v,
431	    cv_add(1n, Nat.mul(3n, Nat.add(y, b)), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 3n, 3n}, v, cv_c(1n, v), cv_mul(3n, Nat.add(y, b), L{0n, 0n, 0n, 1n, 1n}, v, cv_add(y, b, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 0n, 0n, 1n}, v, cv_3(l, x, y, b), cv_4(l, x, y, b)))),
432	    cv_add(l, x, L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_1(l, x, y, b), cv_2(l, x, y, b)), ng)
433	  +f_h1 = cvle(Nat.add(x, y), Nat.mul(3n, b), L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, v,
434	    cv_add(x, y, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(l, x, y, b), cv_3(l, x, y, b)),
435	    cv_mul(3n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b)), h1)
436	  +f_h3 = cvle(1n+Nat.mul(3n, l), Nat.add(Nat.add(x, y), b), L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 1n}, v,
437	    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, x, y, b))),
438	    cv_add(Nat.add(x, y), b, L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 1n}, v, cv_add(x, y, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(l, x, y, b), cv_3(l, x, y, b)), cv_4(l, x, y, b)), h3)
439	  +f_h5 = cvle(x, Nat.mul(3n, y), L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v,
440	    cv_2(l, x, y, b),
441	    cv_mul(3n, y, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(l, x, y, b)), h5)
442	  contra(L{3n, 3n, 3n, 7n, 6n}, L{0n, 2n, 3n, 7n, 4n}, v,
443	    comb(L{2n, 0n, 0n, 6n, 6n}, L{0n, 2n, 2n, 0n, 0n}, L{1n, 3n, 3n, 1n, 0n}, L{0n, 0n, 1n, 7n, 4n}, v, scale(2n, L{1n, 0n, 0n, 3n, 3n}, L{0n, 1n, 1n, 0n, 0n}, v, f_ng),
444	    comb(L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, L{1n, 3n, 2n, 0n, 0n}, L{0n, 0n, 1n, 7n, 1n}, v, f_h1,
445	    comb(L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 1n}, L{0n, 0n, 2n, 0n, 0n}, L{0n, 0n, 0n, 6n, 0n}, v, f_h3,
446	    scale(2n, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v, f_h5)))), {==})
447	def rld.c0b(+l: Nat, +x: Nat, +y: Nat, +b: Nat, h1: LE(Nat.add(x, y), Nat.mul(3n, b)), h3: LE(1n+Nat.mul(3n, l), Nat.add(Nat.add(x, y), b)), h5: LE(x, Nat.mul(3n, y))) -> LE(Nat.add(l, x), Nat.mul(3n, Nat.add(y, b))):
448	  by_contra(Nat.add(l, x), Nat.mul(3n, Nat.add(y, b)), ng => rld.c0b.k(l, x, y, b, ng, h1, h3, h5))
449	
450	def rld.w0(+l: Nat, +x: Nat, +y: Nat, +b: Nat, +h1: LE(Nat.add(x, y), Nat.mul(3n, b)), +h2: LE(b, Nat.mul(3n, Nat.add(x, y))), +h3: LE(1n+Nat.mul(3n, l), Nat.add(Nat.add(x, y), b)), +h4: LE(Nat.add(Nat.add(x, y), b), Nat.add(3n, Nat.mul(3n, l))), +hd: LE(Nat.mul(2n, b), Nat.add(x, y)), +h5: LE(x, Nat.mul(3n, y)), +h6: LE(y, Nat.mul(3n, x)), +pl: LE(1n, l), +px: LE(1n, x), +py: LE(1n, y), +pb: LE(1n, b)) -> {wok(Nat.add(l, x), Nat.add(y, b)) == True{} : Bool}:
451	  MBool.and_eq_true(Nat.is_le(Nat.add(y, b), Nat.mul(3n, Nat.add(l, x))), Nat.is_le(Nat.add(l, x), Nat.mul(3n, Nat.add(y, b))), rld.c0a(l, x, y, b, h4, px), rld.c0b(l, x, y, b, h1, h3, h5))
452	
453	def rld.c1a.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, l), x), h1: LE(Nat.add(x, y), Nat.mul(3n, b)), h4: LE(Nat.add(Nat.add(x, y), b), Nat.add(3n, Nat.mul(3n, l))), pl: LE(1n, l), py: LE(1n, y)) -> Empty:
454	  +v = {VS{l, x, y, b} : Vs}
455	  +f_ng = cvle(1n+Nat.mul(3n, l), x, L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v,
456	    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, x, y, b))),
457	    cv_2(l, x, y, b), ng)
458	  +f_h1 = cvle(Nat.add(x, y), Nat.mul(3n, b), L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, v,
459	    cv_add(x, y, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(l, x, y, b), cv_3(l, x, y, b)),
460	    cv_mul(3n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b)), h1)
461	  +f_h4 = cvle(Nat.add(Nat.add(x, y), b), Nat.add(3n, Nat.mul(3n, l)), L{0n, 0n, 1n, 1n, 1n}, L{3n, 3n, 0n, 0n, 0n}, v,
462	    cv_add(Nat.add(x, y), b, L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 1n}, v, cv_add(x, y, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(l, x, y, b), cv_3(l, x, y, b)), cv_4(l, x, y, b)),
463	    cv_add(3n, Nat.mul(3n, l), L{3n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(3n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, x, y, b))), h4)
464	  +f_pl = cvle(1n, l, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
465	    cv_c(1n, v),
466	    cv_1(l, x, y, b), pl)
467	  +f_py = cvle(1n, y, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v,
468	    cv_c(1n, v),
469	    cv_3(l, x, y, b), py)
470	  contra(L{10n, 12n, 4n, 4n, 3n}, L{9n, 11n, 4n, 4n, 3n}, v,
471	    comb(L{4n, 12n, 0n, 0n, 0n}, L{0n, 0n, 4n, 0n, 0n}, L{6n, 0n, 4n, 4n, 3n}, L{9n, 11n, 0n, 4n, 3n}, v, scale(4n, L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, f_ng),
472	    comb(L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, L{6n, 0n, 3n, 3n, 3n}, L{9n, 11n, 0n, 4n, 0n}, v, f_h1,
473	    comb(L{0n, 0n, 3n, 3n, 3n}, L{9n, 9n, 0n, 0n, 0n}, L{6n, 0n, 0n, 0n, 0n}, L{0n, 2n, 0n, 4n, 0n}, v, scale(3n, L{0n, 0n, 1n, 1n, 1n}, L{3n, 3n, 0n, 0n, 0n}, v, f_h4),
474	    comb(L{2n, 0n, 0n, 0n, 0n}, L{0n, 2n, 0n, 0n, 0n}, L{4n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 4n, 0n}, v, scale(2n, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, f_pl),
475	    scale(4n, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, f_py))))), {==})
476	def rld.c1a(+l: Nat, +x: Nat, +y: Nat, +b: Nat, h1: LE(Nat.add(x, y), Nat.mul(3n, b)), h4: LE(Nat.add(Nat.add(x, y), b), Nat.add(3n, Nat.mul(3n, l))), pl: LE(1n, l), py: LE(1n, y)) -> LE(x, Nat.mul(3n, l)):
477	  by_contra(x, Nat.mul(3n, l), ng => rld.c1a.k(l, x, y, b, ng, h1, h4, pl, py))
478	
479	def rld.c1b.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, x), l), h3: LE(1n+Nat.mul(3n, l), Nat.add(Nat.add(x, y), b)), hd: LE(Nat.mul(2n, b), Nat.add(x, y)), h6: LE(y, Nat.mul(3n, x))) -> Empty:
480	  +v = {VS{l, x, y, b} : Vs}
481	  +f_ng = cvle(1n+Nat.mul(3n, x), l, L{1n, 0n, 3n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
482	    cv_add(1n, Nat.mul(3n, x), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, x, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(l, x, y, b))),
483	    cv_1(l, x, y, b), ng)
484	  +f_h3 = cvle(1n+Nat.mul(3n, l), Nat.add(Nat.add(x, y), b), L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 1n}, v,
485	    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, x, y, b))),
486	    cv_add(Nat.add(x, y), b, L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 1n}, v, cv_add(x, y, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(l, x, y, b), cv_3(l, x, y, b)), cv_4(l, x, y, b)), h3)
487	  +f_hd = cvle(Nat.mul(2n, b), Nat.add(x, y), L{0n, 0n, 0n, 0n, 2n}, L{0n, 0n, 1n, 1n, 0n}, v,
488	    cv_mul(2n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b)),
489	    cv_add(x, y, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(l, x, y, b), cv_3(l, x, y, b)), hd)
490	  +f_h6 = cvle(y, Nat.mul(3n, x), L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v,
491	    cv_3(l, x, y, b),
492	    cv_mul(3n, x, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(l, x, y, b)), h6)
493	  contra(L{4n, 3n, 9n, 2n, 2n}, L{0n, 3n, 8n, 2n, 1n}, v,
494	    comb(L{3n, 0n, 9n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, L{1n, 3n, 0n, 2n, 2n}, L{0n, 0n, 8n, 2n, 1n}, v, scale(3n, L{1n, 0n, 3n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, f_ng),
495	    comb(L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 1n}, L{0n, 0n, 0n, 2n, 2n}, L{0n, 0n, 7n, 1n, 0n}, v, f_h3,
496	    comb(L{0n, 0n, 0n, 0n, 2n}, L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 2n, 0n}, L{0n, 0n, 6n, 0n, 0n}, v, f_hd,
497	    scale(2n, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v, f_h6)))), {==})
498	def rld.c1b(+l: Nat, +x: Nat, +y: Nat, +b: Nat, h3: LE(1n+Nat.mul(3n, l), Nat.add(Nat.add(x, y), b)), hd: LE(Nat.mul(2n, b), Nat.add(x, y)), h6: LE(y, Nat.mul(3n, x))) -> LE(l, Nat.mul(3n, x)):
499	  by_contra(l, Nat.mul(3n, x), ng => rld.c1b.k(l, x, y, b, ng, h3, hd, h6))
500	
501	def rld.w1(+l: Nat, +x: Nat, +y: Nat, +b: Nat, +h1: LE(Nat.add(x, y), Nat.mul(3n, b)), +h2: LE(b, Nat.mul(3n, Nat.add(x, y))), +h3: LE(1n+Nat.mul(3n, l), Nat.add(Nat.add(x, y), b)), +h4: LE(Nat.add(Nat.add(x, y), b), Nat.add(3n, Nat.mul(3n, l))), +hd: LE(Nat.mul(2n, b), Nat.add(x, y)), +h5: LE(x, Nat.mul(3n, y)), +h6: LE(y, Nat.mul(3n, x)), +pl: LE(1n, l), +px: LE(1n, x), +py: LE(1n, y), +pb: LE(1n, b)) -> {wok(l, x) == True{} : Bool}:
502	  MBool.and_eq_true(Nat.is_le(x, Nat.mul(3n, l)), Nat.is_le(l, Nat.mul(3n, x)), rld.c1a(l, x, y, b, h1, h4, pl, py), rld.c1b(l, x, y, b, h3, hd, h6))
503	
504	def rld.c2a.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, y), b), hd: LE(Nat.mul(2n, b), Nat.add(x, y)), h5: LE(x, Nat.mul(3n, y))) -> Empty:
505	  +v = {VS{l, x, y, b} : Vs}
506	  +f_ng = cvle(1n+Nat.mul(3n, y), b, L{1n, 0n, 0n, 3n, 0n}, L{0n, 0n, 0n, 0n, 1n}, v,
507	    cv_add(1n, Nat.mul(3n, y), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v, cv_c(1n, v), cv_mul(3n, y, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(l, x, y, b))),
508	    cv_4(l, x, y, b), ng)
509	  +f_hd = cvle(Nat.mul(2n, b), Nat.add(x, y), L{0n, 0n, 0n, 0n, 2n}, L{0n, 0n, 1n, 1n, 0n}, v,
510	    cv_mul(2n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b)),
511	    cv_add(x, y, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(l, x, y, b), cv_3(l, x, y, b)), hd)
512	  +f_h5 = cvle(x, Nat.mul(3n, y), L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v,
513	    cv_2(l, x, y, b),
514	    cv_mul(3n, y, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(l, x, y, b)), h5)
515	  contra(L{2n, 0n, 1n, 6n, 2n}, L{0n, 0n, 1n, 4n, 2n}, v,
516	    comb(L{2n, 0n, 0n, 6n, 0n}, L{0n, 0n, 0n, 0n, 2n}, L{0n, 0n, 1n, 0n, 2n}, L{0n, 0n, 1n, 4n, 0n}, v, scale(2n, L{1n, 0n, 0n, 3n, 0n}, L{0n, 0n, 0n, 0n, 1n}, v, f_ng),
517	    comb(L{0n, 0n, 0n, 0n, 2n}, L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v, f_hd,
518	    f_h5)), {==})
519	def rld.c2a(+l: Nat, +x: Nat, +y: Nat, +b: Nat, hd: LE(Nat.mul(2n, b), Nat.add(x, y)), h5: LE(x, Nat.mul(3n, y))) -> LE(b, Nat.mul(3n, y)):
520	  by_contra(b, Nat.mul(3n, y), ng => rld.c2a.k(l, x, y, b, ng, hd, h5))
521	
522	def rld.c2b.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, b), y), h1: LE(Nat.add(x, y), Nat.mul(3n, b))) -> Empty:
523	  +v = {VS{l, x, y, b} : Vs}
524	  +f_ng = cvle(1n+Nat.mul(3n, b), y, L{1n, 0n, 0n, 0n, 3n}, L{0n, 0n, 0n, 1n, 0n}, v,
525	    cv_add(1n, Nat.mul(3n, b), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 0n, 3n}, v, cv_c(1n, v), cv_mul(3n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b))),
526	    cv_3(l, x, y, b), ng)
527	  +f_h1 = cvle(Nat.add(x, y), Nat.mul(3n, b), L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, v,
528	    cv_add(x, y, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(l, x, y, b), cv_3(l, x, y, b)),
529	    cv_mul(3n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b)), h1)
530	  contra(L{1n, 0n, 1n, 1n, 3n}, L{0n, 0n, 0n, 1n, 3n}, v,
531	    comb(L{1n, 0n, 0n, 0n, 3n}, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, v, f_ng,
532	    f_h1), {==})
533	def rld.c2b(+l: Nat, +x: Nat, +y: Nat, +b: Nat, h1: LE(Nat.add(x, y), Nat.mul(3n, b))) -> LE(y, Nat.mul(3n, b)):
534	  by_contra(y, Nat.mul(3n, b), ng => rld.c2b.k(l, x, y, b, ng, h1))
535	
536	def rld.w2(+l: Nat, +x: Nat, +y: Nat, +b: Nat, +h1: LE(Nat.add(x, y), Nat.mul(3n, b)), +h2: LE(b, Nat.mul(3n, Nat.add(x, y))), +h3: LE(1n+Nat.mul(3n, l), Nat.add(Nat.add(x, y), b)), +h4: LE(Nat.add(Nat.add(x, y), b), Nat.add(3n, Nat.mul(3n, l))), +hd: LE(Nat.mul(2n, b), Nat.add(x, y)), +h5: LE(x, Nat.mul(3n, y)), +h6: LE(y, Nat.mul(3n, x)), +pl: LE(1n, l), +px: LE(1n, x), +py: LE(1n, y), +pb: LE(1n, b)) -> {wok(y, b) == True{} : Bool}:
537	  MBool.and_eq_true(Nat.is_le(b, Nat.mul(3n, y)), Nat.is_le(y, Nat.mul(3n, b)), rld.c2a(l, x, y, b, hd, h5), rld.c2b(l, x, y, b, h1))
538	
539	def rhd.c0a.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, Nat.add(b, y)), Nat.add(x, l)), h1: LE(Nat.add(y, x), Nat.mul(3n, b)), h3: LE(1n+Nat.mul(3n, l), Nat.add(b, Nat.add(y, x))), h5: LE(x, Nat.mul(3n, y))) -> Empty:
540	  +v = {VS{l, x, y, b} : Vs}
541	  +f_ng = cvle(1n+Nat.mul(3n, Nat.add(b, y)), Nat.add(x, l), L{1n, 0n, 0n, 3n, 3n}, L{0n, 1n, 1n, 0n, 0n}, v,
542	    cv_add(1n, Nat.mul(3n, Nat.add(b, y)), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 3n, 3n}, v, cv_c(1n, v), cv_mul(3n, Nat.add(b, y), L{0n, 0n, 0n, 1n, 1n}, v, cv_add(b, y, L{0n, 0n, 0n, 0n, 1n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_4(l, x, y, b), cv_3(l, x, y, b)))),
543	    cv_add(x, l, L{0n, 0n, 1n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_2(l, x, y, b), cv_1(l, x, y, b)), ng)
544	  +f_h1 = cvle(Nat.add(y, x), Nat.mul(3n, b), L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, v,
545	    cv_add(y, x, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, x, y, b), cv_2(l, x, y, b)),
546	    cv_mul(3n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b)), h1)
547	  +f_h3 = cvle(1n+Nat.mul(3n, l), Nat.add(b, Nat.add(y, x)), L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 1n}, v,
548	    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, x, y, b))),
549	    cv_add(b, Nat.add(y, x), L{0n, 0n, 0n, 0n, 1n}, L{0n, 0n, 1n, 1n, 0n}, v, cv_4(l, x, y, b), cv_add(y, x, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, x, y, b), cv_2(l, x, y, b))), h3)
550	  +f_h5 = cvle(x, Nat.mul(3n, y), L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v,
551	    cv_2(l, x, y, b),
552	    cv_mul(3n, y, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(l, x, y, b)), h5)
553	  contra(L{3n, 3n, 3n, 7n, 6n}, L{0n, 2n, 3n, 7n, 4n}, v,
554	    comb(L{2n, 0n, 0n, 6n, 6n}, L{0n, 2n, 2n, 0n, 0n}, L{1n, 3n, 3n, 1n, 0n}, L{0n, 0n, 1n, 7n, 4n}, v, scale(2n, L{1n, 0n, 0n, 3n, 3n}, L{0n, 1n, 1n, 0n, 0n}, v, f_ng),
555	    comb(L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, L{1n, 3n, 2n, 0n, 0n}, L{0n, 0n, 1n, 7n, 1n}, v, f_h1,
556	    comb(L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 1n}, L{0n, 0n, 2n, 0n, 0n}, L{0n, 0n, 0n, 6n, 0n}, v, f_h3,
557	    scale(2n, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v, f_h5)))), {==})
558	def rhd.c0a(+l: Nat, +x: Nat, +y: Nat, +b: Nat, h1: LE(Nat.add(y, x), Nat.mul(3n, b)), h3: LE(1n+Nat.mul(3n, l), Nat.add(b, Nat.add(y, x))), h5: LE(x, Nat.mul(3n, y))) -> LE(Nat.add(x, l), Nat.mul(3n, Nat.add(b, y))):
559	  by_contra(Nat.add(x, l), Nat.mul(3n, Nat.add(b, y)), ng => rhd.c0a.k(l, x, y, b, ng, h1, h3, h5))
560	
561	def rhd.c0b.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, Nat.add(x, l)), Nat.add(b, y)), h4: LE(Nat.add(b, Nat.add(y, x)), Nat.add(3n, Nat.mul(3n, l))), px: LE(1n, x)) -> Empty:
562	  +v = {VS{l, x, y, b} : Vs}
563	  +f_ng = cvle(1n+Nat.mul(3n, Nat.add(x, l)), Nat.add(b, y), L{1n, 3n, 3n, 0n, 0n}, L{0n, 0n, 0n, 1n, 1n}, v,
564	    cv_add(1n, Nat.mul(3n, Nat.add(x, l)), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 3n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, Nat.add(x, l), L{0n, 1n, 1n, 0n, 0n}, v, cv_add(x, l, L{0n, 0n, 1n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_2(l, x, y, b), cv_1(l, x, y, b)))),
565	    cv_add(b, y, L{0n, 0n, 0n, 0n, 1n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_4(l, x, y, b), cv_3(l, x, y, b)), ng)
566	  +f_h4 = cvle(Nat.add(b, Nat.add(y, x)), Nat.add(3n, Nat.mul(3n, l)), L{0n, 0n, 1n, 1n, 1n}, L{3n, 3n, 0n, 0n, 0n}, v,
567	    cv_add(b, Nat.add(y, x), L{0n, 0n, 0n, 0n, 1n}, L{0n, 0n, 1n, 1n, 0n}, v, cv_4(l, x, y, b), cv_add(y, x, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, x, y, b), cv_2(l, x, y, b))),
568	    cv_add(3n, Nat.mul(3n, l), L{3n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(3n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, x, y, b))), h4)
569	  +f_px = cvle(1n, x, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v,
570	    cv_c(1n, v),
571	    cv_2(l, x, y, b), px)
572	  contra(L{4n, 3n, 4n, 1n, 1n}, L{3n, 3n, 3n, 1n, 1n}, v,
573	    comb(L{1n, 3n, 3n, 0n, 0n}, L{0n, 0n, 0n, 1n, 1n}, L{3n, 0n, 1n, 1n, 1n}, L{3n, 3n, 3n, 0n, 0n}, v, f_ng,
574	    comb(L{0n, 0n, 1n, 1n, 1n}, L{3n, 3n, 0n, 0n, 0n}, L{3n, 0n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v, f_h4,
575	    scale(3n, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, f_px))), {==})
576	def rhd.c0b(+l: Nat, +x: Nat, +y: Nat, +b: Nat, h4: LE(Nat.add(b, Nat.add(y, x)), Nat.add(3n, Nat.mul(3n, l))), px: LE(1n, x)) -> LE(Nat.add(b, y), Nat.mul(3n, Nat.add(x, l))):
577	  by_contra(Nat.add(b, y), Nat.mul(3n, Nat.add(x, l)), ng => rhd.c0b.k(l, x, y, b, ng, h4, px))
578	
579	def rhd.w0(+l: Nat, +x: Nat, +y: Nat, +b: Nat, +h1: LE(Nat.add(y, x), Nat.mul(3n, b)), +h2: LE(b, Nat.mul(3n, Nat.add(y, x))), +h3: LE(1n+Nat.mul(3n, l), Nat.add(b, Nat.add(y, x))), +h4: LE(Nat.add(b, Nat.add(y, x)), Nat.add(3n, Nat.mul(3n, l))), +hd: LE(Nat.mul(2n, b), Nat.add(y, x)), +h5: LE(x, Nat.mul(3n, y)), +h6: LE(y, Nat.mul(3n, x)), +pl: LE(1n, l), +px: LE(1n, x), +py: LE(1n, y), +pb: LE(1n, b)) -> {wok(Nat.add(b, y), Nat.add(x, l)) == True{} : Bool}:
580	  MBool.and_eq_true(Nat.is_le(Nat.add(x, l), Nat.mul(3n, Nat.add(b, y))), Nat.is_le(Nat.add(b, y), Nat.mul(3n, Nat.add(x, l))), rhd.c0a(l, x, y, b, h1, h3, h5), rhd.c0b(l, x, y, b, h4, px))
581	
582	def rhd.c1a.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, b), y), h1: LE(Nat.add(y, x), Nat.mul(3n, b))) -> Empty:
583	  +v = {VS{l, x, y, b} : Vs}
584	  +f_ng = cvle(1n+Nat.mul(3n, b), y, L{1n, 0n, 0n, 0n, 3n}, L{0n, 0n, 0n, 1n, 0n}, v,
585	    cv_add(1n, Nat.mul(3n, b), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 0n, 3n}, v, cv_c(1n, v), cv_mul(3n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b))),
586	    cv_3(l, x, y, b), ng)
587	  +f_h1 = cvle(Nat.add(y, x), Nat.mul(3n, b), L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, v,
588	    cv_add(y, x, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, x, y, b), cv_2(l, x, y, b)),
589	    cv_mul(3n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b)), h1)
590	  contra(L{1n, 0n, 1n, 1n, 3n}, L{0n, 0n, 0n, 1n, 3n}, v,
591	    comb(L{1n, 0n, 0n, 0n, 3n}, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, v, f_ng,
592	    f_h1), {==})
593	def rhd.c1a(+l: Nat, +x: Nat, +y: Nat, +b: Nat, h1: LE(Nat.add(y, x), Nat.mul(3n, b))) -> LE(y, Nat.mul(3n, b)):
594	  by_contra(y, Nat.mul(3n, b), ng => rhd.c1a.k(l, x, y, b, ng, h1))
595	
596	def rhd.c1b.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, y), b), hd: LE(Nat.mul(2n, b), Nat.add(y, x)), h5: LE(x, Nat.mul(3n, y))) -> Empty:
597	  +v = {VS{l, x, y, b} : Vs}
598	  +f_ng = cvle(1n+Nat.mul(3n, y), b, L{1n, 0n, 0n, 3n, 0n}, L{0n, 0n, 0n, 0n, 1n}, v,
599	    cv_add(1n, Nat.mul(3n, y), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v, cv_c(1n, v), cv_mul(3n, y, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(l, x, y, b))),
600	    cv_4(l, x, y, b), ng)
601	  +f_hd = cvle(Nat.mul(2n, b), Nat.add(y, x), L{0n, 0n, 0n, 0n, 2n}, L{0n, 0n, 1n, 1n, 0n}, v,
602	    cv_mul(2n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b)),
603	    cv_add(y, x, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, x, y, b), cv_2(l, x, y, b)), hd)
604	  +f_h5 = cvle(x, Nat.mul(3n, y), L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v,
605	    cv_2(l, x, y, b),
606	    cv_mul(3n, y, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(l, x, y, b)), h5)
607	  contra(L{2n, 0n, 1n, 6n, 2n}, L{0n, 0n, 1n, 4n, 2n}, v,
608	    comb(L{2n, 0n, 0n, 6n, 0n}, L{0n, 0n, 0n, 0n, 2n}, L{0n, 0n, 1n, 0n, 2n}, L{0n, 0n, 1n, 4n, 0n}, v, scale(2n, L{1n, 0n, 0n, 3n, 0n}, L{0n, 0n, 0n, 0n, 1n}, v, f_ng),
609	    comb(L{0n, 0n, 0n, 0n, 2n}, L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v, f_hd,
610	    f_h5)), {==})
611	def rhd.c1b(+l: Nat, +x: Nat, +y: Nat, +b: Nat, hd: LE(Nat.mul(2n, b), Nat.add(y, x)), h5: LE(x, Nat.mul(3n, y))) -> LE(b, Nat.mul(3n, y)):
612	  by_contra(b, Nat.mul(3n, y), ng => rhd.c1b.k(l, x, y, b, ng, hd, h5))
613	
614	def rhd.w1(+l: Nat, +x: Nat, +y: Nat, +b: Nat, +h1: LE(Nat.add(y, x), Nat.mul(3n, b)), +h2: LE(b, Nat.mul(3n, Nat.add(y, x))), +h3: LE(1n+Nat.mul(3n, l), Nat.add(b, Nat.add(y, x))), +h4: LE(Nat.add(b, Nat.add(y, x)), Nat.add(3n, Nat.mul(3n, l))), +hd: LE(Nat.mul(2n, b), Nat.add(y, x)), +h5: LE(x, Nat.mul(3n, y)), +h6: LE(y, Nat.mul(3n, x)), +pl: LE(1n, l), +px: LE(1n, x), +py: LE(1n, y), +pb: LE(1n, b)) -> {wok(b, y) == True{} : Bool}:
615	  MBool.and_eq_true(Nat.is_le(y, Nat.mul(3n, b)), Nat.is_le(b, Nat.mul(3n, y)), rhd.c1a(l, x, y, b, h1), rhd.c1b(l, x, y, b, hd, h5))
616	
617	def rhd.c2a.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, x), l), h3: LE(1n+Nat.mul(3n, l), Nat.add(b, Nat.add(y, x))), hd: LE(Nat.mul(2n, b), Nat.add(y, x)), h6: LE(y, Nat.mul(3n, x))) -> Empty:
618	  +v = {VS{l, x, y, b} : Vs}
619	  +f_ng = cvle(1n+Nat.mul(3n, x), l, L{1n, 0n, 3n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
620	    cv_add(1n, Nat.mul(3n, x), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, x, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(l, x, y, b))),
621	    cv_1(l, x, y, b), ng)
622	  +f_h3 = cvle(1n+Nat.mul(3n, l), Nat.add(b, Nat.add(y, x)), L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 1n}, v,
623	    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, x, y, b))),
624	    cv_add(b, Nat.add(y, x), L{0n, 0n, 0n, 0n, 1n}, L{0n, 0n, 1n, 1n, 0n}, v, cv_4(l, x, y, b), cv_add(y, x, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, x, y, b), cv_2(l, x, y, b))), h3)
625	  +f_hd = cvle(Nat.mul(2n, b), Nat.add(y, x), L{0n, 0n, 0n, 0n, 2n}, L{0n, 0n, 1n, 1n, 0n}, v,
626	    cv_mul(2n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b)),
627	    cv_add(y, x, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, x, y, b), cv_2(l, x, y, b)), hd)
628	  +f_h6 = cvle(y, Nat.mul(3n, x), L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v,
629	    cv_3(l, x, y, b),
630	    cv_mul(3n, x, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(l, x, y, b)), h6)
631	  contra(L{4n, 3n, 9n, 2n, 2n}, L{0n, 3n, 8n, 2n, 1n}, v,
632	    comb(L{3n, 0n, 9n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, L{1n, 3n, 0n, 2n, 2n}, L{0n, 0n, 8n, 2n, 1n}, v, scale(3n, L{1n, 0n, 3n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, f_ng),
633	    comb(L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 1n}, L{0n, 0n, 0n, 2n, 2n}, L{0n, 0n, 7n, 1n, 0n}, v, f_h3,
634	    comb(L{0n, 0n, 0n, 0n, 2n}, L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 2n, 0n}, L{0n, 0n, 6n, 0n, 0n}, v, f_hd,
635	    scale(2n, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v, f_h6)))), {==})
636	def rhd.c2a(+l: Nat, +x: Nat, +y: Nat, +b: Nat, h3: LE(1n+Nat.mul(3n, l), Nat.add(b, Nat.add(y, x))), hd: LE(Nat.mul(2n, b), Nat.add(y, x)), h6: LE(y, Nat.mul(3n, x))) -> LE(l, Nat.mul(3n, x)):
637	  by_contra(l, Nat.mul(3n, x), ng => rhd.c2a.k(l, x, y, b, ng, h3, hd, h6))
638	
639	def rhd.c2b.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, l), x), h1: LE(Nat.add(y, x), Nat.mul(3n, b)), h4: LE(Nat.add(b, Nat.add(y, x)), Nat.add(3n, Nat.mul(3n, l))), pl: LE(1n, l), py: LE(1n, y)) -> Empty:
640	  +v = {VS{l, x, y, b} : Vs}
641	  +f_ng = cvle(1n+Nat.mul(3n, l), x, L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v,
642	    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, x, y, b))),
643	    cv_2(l, x, y, b), ng)
644	  +f_h1 = cvle(Nat.add(y, x), Nat.mul(3n, b), L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, v,
645	    cv_add(y, x, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, x, y, b), cv_2(l, x, y, b)),
646	    cv_mul(3n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b)), h1)
647	  +f_h4 = cvle(Nat.add(b, Nat.add(y, x)), Nat.add(3n, Nat.mul(3n, l)), L{0n, 0n, 1n, 1n, 1n}, L{3n, 3n, 0n, 0n, 0n}, v,
648	    cv_add(b, Nat.add(y, x), L{0n, 0n, 0n, 0n, 1n}, L{0n, 0n, 1n, 1n, 0n}, v, cv_4(l, x, y, b), cv_add(y, x, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, x, y, b), cv_2(l, x, y, b))),
649	    cv_add(3n, Nat.mul(3n, l), L{3n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(3n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, x, y, b))), h4)
650	  +f_pl = cvle(1n, l, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
651	    cv_c(1n, v),
652	    cv_1(l, x, y, b), pl)
653	  +f_py = cvle(1n, y, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v,
654	    cv_c(1n, v),
655	    cv_3(l, x, y, b), py)
656	  contra(L{10n, 12n, 4n, 4n, 3n}, L{9n, 11n, 4n, 4n, 3n}, v,
657	    comb(L{4n, 12n, 0n, 0n, 0n}, L{0n, 0n, 4n, 0n, 0n}, L{6n, 0n, 4n, 4n, 3n}, L{9n, 11n, 0n, 4n, 3n}, v, scale(4n, L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, f_ng),
658	    comb(L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, L{6n, 0n, 3n, 3n, 3n}, L{9n, 11n, 0n, 4n, 0n}, v, f_h1,
659	    comb(L{0n, 0n, 3n, 3n, 3n}, L{9n, 9n, 0n, 0n, 0n}, L{6n, 0n, 0n, 0n, 0n}, L{0n, 2n, 0n, 4n, 0n}, v, scale(3n, L{0n, 0n, 1n, 1n, 1n}, L{3n, 3n, 0n, 0n, 0n}, v, f_h4),
660	    comb(L{2n, 0n, 0n, 0n, 0n}, L{0n, 2n, 0n, 0n, 0n}, L{4n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 4n, 0n}, v, scale(2n, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, f_pl),
661	    scale(4n, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, f_py))))), {==})
662	def rhd.c2b(+l: Nat, +x: Nat, +y: Nat, +b: Nat, h1: LE(Nat.add(y, x), Nat.mul(3n, b)), h4: LE(Nat.add(b, Nat.add(y, x)), Nat.add(3n, Nat.mul(3n, l))), pl: LE(1n, l), py: LE(1n, y)) -> LE(x, Nat.mul(3n, l)):
663	  by_contra(x, Nat.mul(3n, l), ng => rhd.c2b.k(l, x, y, b, ng, h1, h4, pl, py))
664	
665	def rhd.w2(+l: Nat, +x: Nat, +y: Nat, +b: Nat, +h1: LE(Nat.add(y, x), Nat.mul(3n, b)), +h2: LE(b, Nat.mul(3n, Nat.add(y, x))), +h3: LE(1n+Nat.mul(3n, l), Nat.add(b, Nat.add(y, x))), +h4: LE(Nat.add(b, Nat.add(y, x)), Nat.add(3n, Nat.mul(3n, l))), +hd: LE(Nat.mul(2n, b), Nat.add(y, x)), +h5: LE(x, Nat.mul(3n, y)), +h6: LE(y, Nat.mul(3n, x)), +pl: LE(1n, l), +px: LE(1n, x), +py: LE(1n, y), +pb: LE(1n, b)) -> {wok(x, l) == True{} : Bool}:
666	  MBool.and_eq_true(Nat.is_le(l, Nat.mul(3n, x)), Nat.is_le(x, Nat.mul(3n, l)), rhd.c2a(l, x, y, b, h3, hd, h6), rhd.c2b(l, x, y, b, h1, h4, pl, py))
667	
668	def tiph(+l: Nat, h: LE(1n+Nat.mul(3n, l), 1n), pl: LE(1n, l)) -> Empty:
669	  +v = {VS{l, 0n, 0n, 0n} : Vs}
670	  +f_h = cvle(1n+Nat.mul(3n, l), 1n, L{1n, 3n, 0n, 0n, 0n}, L{1n, 0n, 0n, 0n, 0n}, v,
671	    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, 0n, 0n, 0n))),
672	    cv_c(1n, v), h)
673	  +f_pl = cvle(1n, l, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
674	    cv_c(1n, v),
675	    cv_1(l, 0n, 0n, 0n), pl)
676	  contra(L{2n, 3n, 0n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v,
677	    comb(L{1n, 3n, 0n, 0n, 0n}, L{1n, 0n, 0n, 0n, 0n}, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, f_h,
678	    f_pl), {==})
679	
680	def dtip(+b: Nat, h: LE(Nat.mul(2n, b), 1n), pb: LE(1n, b)) -> Empty:
681	  +v = {VS{b, 0n, 0n, 0n} : Vs}
682	  +f_h = cvle(Nat.mul(2n, b), 1n, L{0n, 2n, 0n, 0n, 0n}, L{1n, 0n, 0n, 0n, 0n}, v,
683	    cv_mul(2n, b, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(b, 0n, 0n, 0n)),
684	    cv_c(1n, v), h)
685	  +f_pb = cvle(1n, b, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
686	    cv_c(1n, v),
687	    cv_1(b, 0n, 0n, 0n), pb)
688	  contra(L{2n, 2n, 0n, 0n, 0n}, L{1n, 2n, 0n, 0n, 0n}, v,
689	    comb(L{0n, 2n, 0n, 0n, 0n}, L{1n, 0n, 0n, 0n, 0n}, L{2n, 0n, 0n, 0n, 0n}, L{0n, 2n, 0n, 0n, 0n}, v, f_h,
690	    scale(2n, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, f_pb)), {==})
691	
692	def almlo.c0a.k(+wl: Nat, +wh: Nat, +w2: Nat, ng: LE(1n+Nat.add(3n, Nat.mul(3n, w2)), wh), o1: LE(wh, Nat.mul(3n, wl)), n1: LE(wl, 1n+w2)) -> Empty:
693	  +v = {VS{wl, wh, w2, 0n} : Vs}
694	  +f_ng = cvle(1n+Nat.add(3n, Nat.mul(3n, w2)), wh, L{4n, 0n, 0n, 3n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v,
695	    cv_add(1n, Nat.add(3n, Nat.mul(3n, w2)), L{1n, 0n, 0n, 0n, 0n}, L{3n, 0n, 0n, 3n, 0n}, v, cv_c(1n, v), cv_add(3n, Nat.mul(3n, w2), L{3n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v, cv_c(3n, v), cv_mul(3n, w2, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(wl, wh, w2, 0n)))),
696	    cv_2(wl, wh, w2, 0n), ng)
697	  +f_o1 = cvle(wh, Nat.mul(3n, wl), L{0n, 0n, 1n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v,
698	    cv_2(wl, wh, w2, 0n),
699	    cv_mul(3n, wl, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(wl, wh, w2, 0n)), o1)
700	  +f_n1 = cvle(wl, 1n+w2, L{0n, 1n, 0n, 0n, 0n}, L{1n, 0n, 0n, 1n, 0n}, v,
701	    cv_1(wl, wh, w2, 0n),
702	    cv_add(1n, w2, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_c(1n, v), cv_3(wl, wh, w2, 0n)), n1)
703	  contra(L{4n, 3n, 1n, 3n, 0n}, L{3n, 3n, 1n, 3n, 0n}, v,
704	    comb(L{4n, 0n, 0n, 3n, 0n}, L{0n, 0n, 1n, 0n, 0n}, L{0n, 3n, 1n, 0n, 0n}, L{3n, 3n, 0n, 3n, 0n}, v, f_ng,
705	    comb(L{0n, 0n, 1n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, L{3n, 0n, 0n, 3n, 0n}, v, f_o1,
706	    scale(3n, L{0n, 1n, 0n, 0n, 0n}, L{1n, 0n, 0n, 1n, 0n}, v, f_n1))), {==})
707	def almlo.c0a(+wl: Nat, +wh: Nat, +w2: Nat, o1: LE(wh, Nat.mul(3n, wl)), n1: LE(wl, 1n+w2)) -> LE(wh, Nat.add(3n, Nat.mul(3n, w2))):
708	  by_contra(wh, Nat.add(3n, Nat.mul(3n, w2)), ng => almlo.c0a.k(wl, wh, w2, ng, o1, n1))
709	
710	def almlo.c0b.k(+wl: Nat, +wh: Nat, +w2: Nat, ng: LE(1n+Nat.add(3n, Nat.mul(3n, wh)), w2), o2: LE(wl, Nat.mul(3n, wh)), n2: LE(w2, 1n+wl)) -> Empty:
711	  +v = {VS{wl, wh, w2, 0n} : Vs}
712	  +f_ng = cvle(1n+Nat.add(3n, Nat.mul(3n, wh)), w2, L{4n, 0n, 3n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v,
713	    cv_add(1n, Nat.add(3n, Nat.mul(3n, wh)), L{1n, 0n, 0n, 0n, 0n}, L{3n, 0n, 3n, 0n, 0n}, v, cv_c(1n, v), cv_add(3n, Nat.mul(3n, wh), L{3n, 0n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v, cv_c(3n, v), cv_mul(3n, wh, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(wl, wh, w2, 0n)))),
714	    cv_3(wl, wh, w2, 0n), ng)
715	  +f_o2 = cvle(wl, Nat.mul(3n, wh), L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v,
716	    cv_1(wl, wh, w2, 0n),
717	    cv_mul(3n, wh, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(wl, wh, w2, 0n)), o2)
718	  +f_n2 = cvle(w2, 1n+wl, L{0n, 0n, 0n, 1n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v,
719	    cv_3(wl, wh, w2, 0n),
720	    cv_add(1n, wl, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_1(wl, wh, w2, 0n)), n2)
721	  contra(L{4n, 1n, 3n, 1n, 0n}, L{1n, 1n, 3n, 1n, 0n}, v,
722	    comb(L{4n, 0n, 3n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, L{0n, 1n, 0n, 1n, 0n}, L{1n, 1n, 3n, 0n, 0n}, v, f_ng,
723	    comb(L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v, f_o2,
724	    f_n2)), {==})
725	def almlo.c0b(+wl: Nat, +wh: Nat, +w2: Nat, o2: LE(wl, Nat.mul(3n, wh)), n2: LE(w2, 1n+wl)) -> LE(w2, Nat.add(3n, Nat.mul(3n, wh))):
726	  by_contra(w2, Nat.add(3n, Nat.mul(3n, wh)), ng => almlo.c0b.k(wl, wh, w2, ng, o2, n2))
727	
728	def almlo.w0(+wl: Nat, +wh: Nat, +w2: Nat, +o1: LE(wh, Nat.mul(3n, wl)), +o2: LE(wl, Nat.mul(3n, wh)), +n1: LE(wl, 1n+w2), +n2: LE(w2, 1n+wl)) -> {alm(w2, wh) == True{} : Bool}:
729	  MBool.and_eq_true(Nat.is_le(wh, Nat.add(3n, Nat.mul(3n, w2))), Nat.is_le(w2, Nat.add(3n, Nat.mul(3n, wh))), almlo.c0a(wl, wh, w2, o1, n1), almlo.c0b(wl, wh, w2, o2, n2))
730	
731	def almhi.c0a.k(+wl: Nat, +wh: Nat, +w2: Nat, ng: LE(1n+Nat.add(3n, Nat.mul(3n, wl)), w2), o1: LE(wh, Nat.mul(3n, wl)), n2: LE(w2, 1n+wh)) -> Empty:
732	  +v = {VS{wl, wh, w2, 0n} : Vs}
733	  +f_ng = cvle(1n+Nat.add(3n, Nat.mul(3n, wl)), w2, L{4n, 3n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v,
734	    cv_add(1n, Nat.add(3n, Nat.mul(3n, wl)), L{1n, 0n, 0n, 0n, 0n}, L{3n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_add(3n, Nat.mul(3n, wl), L{3n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(3n, v), cv_mul(3n, wl, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(wl, wh, w2, 0n)))),
735	    cv_3(wl, wh, w2, 0n), ng)
736	  +f_o1 = cvle(wh, Nat.mul(3n, wl), L{0n, 0n, 1n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v,
737	    cv_2(wl, wh, w2, 0n),
738	    cv_mul(3n, wl, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(wl, wh, w2, 0n)), o1)
739	  +f_n2 = cvle(w2, 1n+wh, L{0n, 0n, 0n, 1n, 0n}, L{1n, 0n, 1n, 0n, 0n}, v,
740	    cv_3(wl, wh, w2, 0n),
741	    cv_add(1n, wh, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_c(1n, v), cv_2(wl, wh, w2, 0n)), n2)
742	  contra(L{4n, 3n, 1n, 1n, 0n}, L{1n, 3n, 1n, 1n, 0n}, v,
743	    comb(L{4n, 3n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 1n, 0n}, L{1n, 3n, 1n, 0n, 0n}, v, f_ng,
744	    comb(L{0n, 0n, 1n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, L{1n, 0n, 1n, 0n, 0n}, v, f_o1,
745	    f_n2)), {==})
746	def almhi.c0a(+wl: Nat, +wh: Nat, +w2: Nat, o1: LE(wh, Nat.mul(3n, wl)), n2: LE(w2, 1n+wh)) -> LE(w2, Nat.add(3n, Nat.mul(3n, wl))):
747	  by_contra(w2, Nat.add(3n, Nat.mul(3n, wl)), ng => almhi.c0a.k(wl, wh, w2, ng, o1, n2))
748	
749	def almhi.c0b.k(+wl: Nat, +wh: Nat, +w2: Nat, ng: LE(1n+Nat.add(3n, Nat.mul(3n, w2)), wl), o2: LE(wl, Nat.mul(3n, wh)), n1: LE(wh, 1n+w2)) -> Empty:
750	  +v = {VS{wl, wh, w2, 0n} : Vs}
751	  +f_ng = cvle(1n+Nat.add(3n, Nat.mul(3n, w2)), wl, L{4n, 0n, 0n, 3n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
752	    cv_add(1n, Nat.add(3n, Nat.mul(3n, w2)), L{1n, 0n, 0n, 0n, 0n}, L{3n, 0n, 0n, 3n, 0n}, v, cv_c(1n, v), cv_add(3n, Nat.mul(3n, w2), L{3n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v, cv_c(3n, v), cv_mul(3n, w2, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(wl, wh, w2, 0n)))),
753	    cv_1(wl, wh, w2, 0n), ng)
754	  +f_o2 = cvle(wl, Nat.mul(3n, wh), L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v,
755	    cv_1(wl, wh, w2, 0n),
756	    cv_mul(3n, wh, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(wl, wh, w2, 0n)), o2)
757	  +f_n1 = cvle(wh, 1n+w2, L{0n, 0n, 1n, 0n, 0n}, L{1n, 0n, 0n, 1n, 0n}, v,
758	    cv_2(wl, wh, w2, 0n),
759	    cv_add(1n, w2, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_c(1n, v), cv_3(wl, wh, w2, 0n)), n1)
760	  contra(L{4n, 1n, 3n, 3n, 0n}, L{3n, 1n, 3n, 3n, 0n}, v,
761	    comb(L{4n, 0n, 0n, 3n, 0n}, L{0n, 1n, 0n, 0n, 0n}, L{0n, 1n, 3n, 0n, 0n}, L{3n, 0n, 3n, 3n, 0n}, v, f_ng,
762	    comb(L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, L{3n, 0n, 0n, 3n, 0n}, v, f_o2,
763	    scale(3n, L{0n, 0n, 1n, 0n, 0n}, L{1n, 0n, 0n, 1n, 0n}, v, f_n1))), {==})
764	def almhi.c0b(+wl: Nat, +wh: Nat, +w2: Nat, o2: LE(wl, Nat.mul(3n, wh)), n1: LE(wh, 1n+w2)) -> LE(wl, Nat.add(3n, Nat.mul(3n, w2))):
765	  by_contra(wl, Nat.add(3n, Nat.mul(3n, w2)), ng => almhi.c0b.k(wl, wh, w2, ng, o2, n1))
766	
767	def almhi.w0(+wl: Nat, +wh: Nat, +w2: Nat, +o1: LE(wh, Nat.mul(3n, wl)), +o2: LE(wl, Nat.mul(3n, wh)), +n1: LE(wh, 1n+w2), +n2: LE(w2, 1n+wh)) -> {alm(wl, w2) == True{} : Bool}:
768	  MBool.and_eq_true(Nat.is_le(w2, Nat.add(3n, Nat.mul(3n, wl))), Nat.is_le(wl, Nat.add(3n, Nat.mul(3n, w2))), almhi.c0a(wl, wh, w2, o1, n2), almhi.c0b(wl, wh, w2, o2, n1))
769	
770	def nearlo.c0a.k(+a: Nat, +a2: Nat, +c: Nat, ng: LE(1n+1n+Nat.add(a2, c), Nat.add(a, c)), n1: LE(a, 1n+a2)) -> Empty:
771	  +v = {VS{a, a2, c, 0n} : Vs}
772	  +f_ng = cvle(1n+1n+Nat.add(a2, c), Nat.add(a, c), L{2n, 0n, 1n, 1n, 0n}, L{0n, 1n, 0n, 1n, 0n}, v,
773	    cv_add(1n, 1n+Nat.add(a2, c), L{1n, 0n, 0n, 0n, 0n}, L{1n, 0n, 1n, 1n, 0n}, v, cv_c(1n, v), cv_add(1n, Nat.add(a2, c), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 0n}, v, cv_c(1n, v), cv_add(a2, c, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(a, a2, c, 0n), cv_3(a, a2, c, 0n)))),
774	    cv_add(a, c, L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_1(a, a2, c, 0n), cv_3(a, a2, c, 0n)), ng)
775	  +f_n1 = cvle(a, 1n+a2, L{0n, 1n, 0n, 0n, 0n}, L{1n, 0n, 1n, 0n, 0n}, v,
776	    cv_1(a, a2, c, 0n),
777	    cv_add(1n, a2, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_c(1n, v), cv_2(a, a2, c, 0n)), n1)
778	  contra(L{2n, 1n, 1n, 1n, 0n}, L{1n, 1n, 1n, 1n, 0n}, v,
779	    comb(L{2n, 0n, 1n, 1n, 0n}, L{0n, 1n, 0n, 1n, 0n}, L{0n, 1n, 0n, 0n, 0n}, L{1n, 0n, 1n, 0n, 0n}, v, f_ng,
780	    f_n1), {==})
781	def nearlo.c0a(+a: Nat, +a2: Nat, +c: Nat, n1: LE(a, 1n+a2)) -> LE(Nat.add(a, c), 1n+Nat.add(a2, c)):
782	  by_contra(Nat.add(a, c), 1n+Nat.add(a2, c), ng => nearlo.c0a.k(a, a2, c, ng, n1))
783	
784	def nearlo.c0b.k(+a: Nat, +a2: Nat, +c: Nat, ng: LE(1n+1n+Nat.add(a, c), Nat.add(a2, c)), n2: LE(a2, 1n+a)) -> Empty:
785	  +v = {VS{a, a2, c, 0n} : Vs}
786	  +f_ng = cvle(1n+1n+Nat.add(a, c), Nat.add(a2, c), L{2n, 1n, 0n, 1n, 0n}, L{0n, 0n, 1n, 1n, 0n}, v,
787	    cv_add(1n, 1n+Nat.add(a, c), L{1n, 0n, 0n, 0n, 0n}, L{1n, 1n, 0n, 1n, 0n}, v, cv_c(1n, v), cv_add(1n, Nat.add(a, c), L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 1n, 0n}, v, cv_c(1n, v), cv_add(a, c, L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_1(a, a2, c, 0n), cv_3(a, a2, c, 0n)))),
788	    cv_add(a2, c, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(a, a2, c, 0n), cv_3(a, a2, c, 0n)), ng)
789	  +f_n2 = cvle(a2, 1n+a, L{0n, 0n, 1n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v,
790	    cv_2(a, a2, c, 0n),
791	    cv_add(1n, a, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_1(a, a2, c, 0n)), n2)
792	  contra(L{2n, 1n, 1n, 1n, 0n}, L{1n, 1n, 1n, 1n, 0n}, v,
793	    comb(L{2n, 1n, 0n, 1n, 0n}, L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v, f_ng,
794	    f_n2), {==})
795	def nearlo.c0b(+a: Nat, +a2: Nat, +c: Nat, n2: LE(a2, 1n+a)) -> LE(Nat.add(a2, c), 1n+Nat.add(a, c)):
796	  by_contra(Nat.add(a2, c), 1n+Nat.add(a, c), ng => nearlo.c0b.k(a, a2, c, ng, n2))
797	
798	def nearlo.w0(+a: Nat, +a2: Nat, +c: Nat, +n1: LE(a, 1n+a2), +n2: LE(a2, 1n+a)) -> {near(Nat.add(a, c), Nat.add(a2, c)) == True{} : Bool}:
799	  MBool.and_eq_true(Nat.is_le(Nat.add(a, c), 1n+Nat.add(a2, c)), Nat.is_le(Nat.add(a2, c), 1n+Nat.add(a, c)), nearlo.c0a(a, a2, c, n1), nearlo.c0b(a, a2, c, n2))
800	
801	def nearhi.c0a.k(+a: Nat, +c: Nat, +c2: Nat, ng: LE(1n+1n+Nat.add(a, c2), Nat.add(a, c)), n1: LE(c, 1n+c2)) -> Empty:
802	  +v = {VS{a, c, c2, 0n} : Vs}
803	  +f_ng = cvle(1n+1n+Nat.add(a, c2), Nat.add(a, c), L{2n, 1n, 0n, 1n, 0n}, L{0n, 1n, 1n, 0n, 0n}, v,
804	    cv_add(1n, 1n+Nat.add(a, c2), L{1n, 0n, 0n, 0n, 0n}, L{1n, 1n, 0n, 1n, 0n}, v, cv_c(1n, v), cv_add(1n, Nat.add(a, c2), L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 1n, 0n}, v, cv_c(1n, v), cv_add(a, c2, L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_1(a, c, c2, 0n), cv_3(a, c, c2, 0n)))),
805	    cv_add(a, c, L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_1(a, c, c2, 0n), cv_2(a, c, c2, 0n)), ng)
806	  +f_n1 = cvle(c, 1n+c2, L{0n, 0n, 1n, 0n, 0n}, L{1n, 0n, 0n, 1n, 0n}, v,
807	    cv_2(a, c, c2, 0n),
808	    cv_add(1n, c2, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_c(1n, v), cv_3(a, c, c2, 0n)), n1)
809	  contra(L{2n, 1n, 1n, 1n, 0n}, L{1n, 1n, 1n, 1n, 0n}, v,
810	    comb(L{2n, 1n, 0n, 1n, 0n}, L{0n, 1n, 1n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, L{1n, 0n, 0n, 1n, 0n}, v, f_ng,
811	    f_n1), {==})
812	def nearhi.c0a(+a: Nat, +c: Nat, +c2: Nat, n1: LE(c, 1n+c2)) -> LE(Nat.add(a, c), 1n+Nat.add(a, c2)):
813	  by_contra(Nat.add(a, c), 1n+Nat.add(a, c2), ng => nearhi.c0a.k(a, c, c2, ng, n1))
814	
815	def nearhi.c0b.k(+a: Nat, +c: Nat, +c2: Nat, ng: LE(1n+1n+Nat.add(a, c), Nat.add(a, c2)), n2: LE(c2, 1n+c)) -> Empty:
816	  +v = {VS{a, c, c2, 0n} : Vs}
817	  +f_ng = cvle(1n+1n+Nat.add(a, c), Nat.add(a, c2), L{2n, 1n, 1n, 0n, 0n}, L{0n, 1n, 0n, 1n, 0n}, v,
818	    cv_add(1n, 1n+Nat.add(a, c), L{1n, 0n, 0n, 0n, 0n}, L{1n, 1n, 1n, 0n, 0n}, v, cv_c(1n, v), cv_add(1n, Nat.add(a, c), L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 1n, 0n, 0n}, v, cv_c(1n, v), cv_add(a, c, L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_1(a, c, c2, 0n), cv_2(a, c, c2, 0n)))),
819	    cv_add(a, c2, L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_1(a, c, c2, 0n), cv_3(a, c, c2, 0n)), ng)
820	  +f_n2 = cvle(c2, 1n+c, L{0n, 0n, 0n, 1n, 0n}, L{1n, 0n, 1n, 0n, 0n}, v,
821	    cv_3(a, c, c2, 0n),
822	    cv_add(1n, c, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_c(1n, v), cv_2(a, c, c2, 0n)), n2)
823	  contra(L{2n, 1n, 1n, 1n, 0n}, L{1n, 1n, 1n, 1n, 0n}, v,
824	    comb(L{2n, 1n, 1n, 0n, 0n}, L{0n, 1n, 0n, 1n, 0n}, L{0n, 0n, 0n, 1n, 0n}, L{1n, 0n, 1n, 0n, 0n}, v, f_ng,
825	    f_n2), {==})
826	def nearhi.c0b(+a: Nat, +c: Nat, +c2: Nat, n2: LE(c2, 1n+c)) -> LE(Nat.add(a, c2), 1n+Nat.add(a, c)):
827	  by_contra(Nat.add(a, c2), 1n+Nat.add(a, c), ng => nearhi.c0b.k(a, c, c2, ng, n2))
828	
829	def nearhi.w0(+a: Nat, +c: Nat, +c2: Nat, +n1: LE(c, 1n+c2), +n2: LE(c2, 1n+c)) -> {near(Nat.add(a, c), Nat.add(a, c2)) == True{} : Bool}:
830	  MBool.and_eq_true(Nat.is_le(Nat.add(a, c), 1n+Nat.add(a, c2)), Nat.is_le(Nat.add(a, c2), 1n+Nat.add(a, c)), nearhi.c0a(a, c, c2, n1), nearhi.c0b(a, c, c2, n2))
831	
832	def nearrf.c0a.k(+a: Nat, ng: LE(1n+1n+a, a)) -> Empty:
833	  +v = {VS{a, 0n, 0n, 0n} : Vs}
834	  +f_ng = cvle(1n+1n+a, a, L{2n, 1n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
835	    cv_add(1n, 1n+a, L{1n, 0n, 0n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_add(1n, a, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_1(a, 0n, 0n, 0n))),
836	    cv_1(a, 0n, 0n, 0n), ng)
837	  contra(L{2n, 1n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
838	    f_ng, {==})
839	def nearrf.c0a(+a: Nat) -> LE(a, 1n+a):
840	  by_contra(a, 1n+a, ng => nearrf.c0a.k(a, ng))
841	
842	def nearrf.c0b.k(+a: Nat, ng: LE(1n+1n+a, a)) -> Empty:
843	  +v = {VS{a, 0n, 0n, 0n} : Vs}
844	  +f_ng = cvle(1n+1n+a, a, L{2n, 1n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
845	    cv_add(1n, 1n+a, L{1n, 0n, 0n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_add(1n, a, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_1(a, 0n, 0n, 0n))),
846	    cv_1(a, 0n, 0n, 0n), ng)
847	  contra(L{2n, 1n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
848	    f_ng, {==})
849	def nearrf.c0b(+a: Nat) -> LE(a, 1n+a):
850	  by_contra(a, 1n+a, ng => nearrf.c0b.k(a, ng))
851	
852	def nearrf.w0(+a: Nat) -> {near(a, a) == True{} : Bool}:
853	  MBool.and_eq_true(Nat.is_le(a, 1n+a), Nat.is_le(a, 1n+a), nearrf.c0a(a), nearrf.c0b(a))
854	
855	def nearpm.c0a.k(+a: Nat, ng: LE(1n+1n+a, 1n+a)) -> Empty:
856	  +v = {VS{a, 0n, 0n, 0n} : Vs}
857	  +f_ng = cvle(1n+1n+a, 1n+a, L{2n, 1n, 0n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v,
858	    cv_add(1n, 1n+a, L{1n, 0n, 0n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_add(1n, a, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_1(a, 0n, 0n, 0n))),
859	    cv_add(1n, a, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_1(a, 0n, 0n, 0n)), ng)
860	  contra(L{2n, 1n, 0n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v,
861	    f_ng, {==})
862	def nearpm.c0a(+a: Nat) -> LE(1n+a, 1n+a):
863	  by_contra(1n+a, 1n+a, ng => nearpm.c0a.k(a, ng))
864	
865	def nearpm.c0b.k(+a: Nat, ng: LE(1n+1n+1n+a, a)) -> Empty:
866	  +v = {VS{a, 0n, 0n, 0n} : Vs}
867	  +f_ng = cvle(1n+1n+1n+a, a, L{3n, 1n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
868	    cv_add(1n, 1n+1n+a, L{1n, 0n, 0n, 0n, 0n}, L{2n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_add(1n, 1n+a, L{1n, 0n, 0n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_add(1n, a, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_1(a, 0n, 0n, 0n)))),
869	    cv_1(a, 0n, 0n, 0n), ng)
870	  contra(L{3n, 1n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
871	    f_ng, {==})
872	def nearpm.c0b(+a: Nat) -> LE(a, 1n+1n+a):
873	  by_contra(a, 1n+1n+a, ng => nearpm.c0b.k(a, ng))
874	
875	def nearpm.w0(+a: Nat) -> {near(1n+a, a) == True{} : Bool}:
876	  MBool.and_eq_true(Nat.is_le(1n+a, 1n+a), Nat.is_le(a, 1n+1n+a), nearpm.c0a(a), nearpm.c0b(a))
877	
878	def neargt.c0a.k(+a: Nat, ng: LE(1n+1n+a, Nat.add(a, 1n))) -> Empty:
879	  +v = {VS{a, 0n, 0n, 0n} : Vs}
880	  +f_ng = cvle(1n+1n+a, Nat.add(a, 1n), L{2n, 1n, 0n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v,
881	    cv_add(1n, 1n+a, L{1n, 0n, 0n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_add(1n, a, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_1(a, 0n, 0n, 0n))),
882	    cv_add(a, 1n, L{0n, 1n, 0n, 0n, 0n}, L{1n, 0n, 0n, 0n, 0n}, v, cv_1(a, 0n, 0n, 0n), cv_c(1n, v)), ng)
883	  contra(L{2n, 1n, 0n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v,
884	    f_ng, {==})
885	def neargt.c0a(+a: Nat) -> LE(Nat.add(a, 1n), 1n+a):
886	  by_contra(Nat.add(a, 1n), 1n+a, ng => neargt.c0a.k(a, ng))
887	
888	def neargt.c0b.k(+a: Nat, ng: LE(1n+1n+Nat.add(a, 1n), a)) -> Empty:
889	  +v = {VS{a, 0n, 0n, 0n} : Vs}
890	  +f_ng = cvle(1n+1n+Nat.add(a, 1n), a, L{3n, 1n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
891	    cv_add(1n, 1n+Nat.add(a, 1n), L{1n, 0n, 0n, 0n, 0n}, L{2n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_add(1n, Nat.add(a, 1n), L{1n, 0n, 0n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_add(a, 1n, L{0n, 1n, 0n, 0n, 0n}, L{1n, 0n, 0n, 0n, 0n}, v, cv_1(a, 0n, 0n, 0n), cv_c(1n, v)))),
892	    cv_1(a, 0n, 0n, 0n), ng)
893	  contra(L{3n, 1n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
894	    f_ng, {==})
895	def neargt.c0b(+a: Nat) -> LE(a, 1n+Nat.add(a, 1n)):
896	  by_contra(a, 1n+Nat.add(a, 1n), ng => neargt.c0b.k(a, ng))
897	
898	def neargt.w0(+a: Nat) -> {near(Nat.add(a, 1n), a) == True{} : Bool}:
899	  MBool.and_eq_true(Nat.is_le(Nat.add(a, 1n), 1n+a), Nat.is_le(a, 1n+Nat.add(a, 1n)), neargt.c0a(a), neargt.c0b(a))