1	# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/listops.src; edit the .src
2	import Base
3	import ../../../spec/lib/common.bend as C
4	import ../../../spec/crypto/secp256k1/field.bend as FS
5	import ../../../src/crypto/secp256k1/limbs.bend as L
6	import ../../lib/nat.bend as N
7	import ../../lib/logic.bend as Lg
8	import ../../lib/lemmas/proofs/nat_algebra.bend as NA
9	import ../../math/natural/arith.bend as NR
10	import ../../math/typed/width.bend as WW
11	import ./semiring.bend as SR
12	import ./limbs.bend as LV
13	import ./ineq.bend as I
14	import ./bounds.bend as B
15	import ./reduce.bend as R
16	
17	# Zero tests, equality, parity, comparison with m and small constants of
18	# src/crypto/secp256k1/limbs.bend, against the values of the limbs.
19	
20	# ---- Bool facts ----
21	
22	def is_eq_add0(a: Nat, +b: Nat) -> {Nat.is_eq(Nat.add(a, b), 0n) == Bool.and(Nat.is_eq(a, 0n), Nat.is_eq(b, 0n)) : Bool}:
23	  match a:
24	    case 0n:
25	      {==}
26	    case 1n+k:
27	      {==}
28	
29	def and_true(+b: Bool) -> {Bool.and(True{}, b) == b : Bool}:
30	  {==}
31	
32	def and_assoc(a: Bool, +b: Bool, +c: Bool) -> {Bool.and(Bool.and(a, b), c) == Bool.and(a, Bool.and(b, c)) : Bool}:
33	  match a:
34	    case True{}:
35	      {==}
36	    case False{}:
37	      {==}
38	
39	# 2^16 y == 0 exactly when y == 0
40	def sh_eq0(+y: Nat) -> {Nat.is_eq(C.shift(16n, y), 0n) == Nat.is_eq(y, 0n) : Bool}:
41	  WW.shift_eq0(16n, y)
42	
43	# ---- is_zero ----
44	
45	def and_true_r(b: Bool) -> {Bool.and(b, True{}) == b : Bool}:
46	  match b:
47	    case True{}:
48	      {==}
49	    case False{}:
50	      {==}
51	
52	
53	def nonzero_v(xs: List<&2, Nat>, +acc: Nat) -> {Nat.is_eq(L.nonzero(xs, acc), 0n) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(LV.ev(xs), 0n)) : Bool}:
54	  match xs:
55	    case Nil{}:
56	      Equal.sym(Bool, Bool.and(Nat.is_eq(acc, 0n), True{}), Nat.is_eq(acc, 0n), and_true_r(Nat.is_eq(acc, 0n)))
57	    case +x <> +t:
58	      %Equal.sym(Bool, Nat.is_eq(L.nonzero(t, Nat.add(acc, x)), 0n), Bool.and(Nat.is_eq(Nat.add(acc, x), 0n), Nat.is_eq(LV.ev(t), 0n)), nonzero_v(t, Nat.add(acc, x))) : {_ == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(t))), 0n)) : Bool}
59	      %Equal.sym(Bool, Nat.is_eq(Nat.add(acc, x), 0n), Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n)), is_eq_add0(acc, x)) : {Bool.and(_, Nat.is_eq(LV.ev(t), 0n)) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(t))), 0n)) : Bool}
60	      %Equal.sym(Bool, Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(t))), 0n), Bool.and(Nat.is_eq(x, 0n), Nat.is_eq(C.shift(16n, LV.ev(t)), 0n)), is_eq_add0(x, C.shift(16n, LV.ev(t)))) : {Bool.and(Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n)), Nat.is_eq(LV.ev(t), 0n)) == Bool.and(Nat.is_eq(acc, 0n), _) : Bool}
61	      %Equal.sym(Bool, Nat.is_eq(C.shift(16n, LV.ev(t)), 0n), Nat.is_eq(LV.ev(t), 0n), sh_eq0(LV.ev(t))) : {Bool.and(Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n)), Nat.is_eq(LV.ev(t), 0n)) == Bool.and(Nat.is_eq(acc, 0n), Bool.and(Nat.is_eq(x, 0n), _)) : Bool}
62	      %Equal.sym(Bool, Bool.and(Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n)), Nat.is_eq(LV.ev(t), 0n)), Bool.and(Nat.is_eq(acc, 0n), Bool.and(Nat.is_eq(x, 0n), Nat.is_eq(LV.ev(t), 0n))), and_assoc(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n), Nat.is_eq(LV.ev(t), 0n))) : {_ == Bool.and(Nat.is_eq(acc, 0n), Bool.and(Nat.is_eq(x, 0n), Nat.is_eq(LV.ev(t), 0n))) : Bool}
63	      {==}
64	
65	def is_zero_v(+xs: List<&2, Nat>) -> {L.is_zero(xs) == Nat.is_eq(LV.ev(xs), 0n) : Bool}:
66	  nonzero_v(xs, 0n)
67	
68	# ---- parity ----
69	
70	def parity_v(+xs: List<&2, Nat>) -> {Nat.mod(L.hd0(xs), 2n) == Nat.mod(LV.ev(xs), 2n) : Nat}:
71	  match xs:
72	    case Nil{}:
73	      {==}
74	    case +x <> +t:
75	      Equal.sym(Nat, Nat.mod(Nat.add(x, C.shift(16n, LV.ev(t))), 2n), Nat.mod(x, 2n), WW.odd_limb(15n, x, LV.ev(t)))
76	
77	# ---- Bool from implications ----
78	
79	def iff_bool(p: Bool, q: Bool, f: {p == True{} : Bool} -> {q == True{} : Bool}, g: {q == True{} : Bool} -> {p == True{} : Bool}) -> {p == q : Bool}:
80	  match p q:
81	    case True{} True{}:
82	      {==}
83	    case False{} False{}:
84	      {==}
85	    case True{} False{}:
86	      Empty.absurd({True{} == False{} : Bool}, Lg.false_true(f({==})))
87	    case False{} True{}:
88	      Empty.absurd({False{} == True{} : Bool}, Lg.false_true(g({==})))
89	
90	# ---- a limb and the rest are unique (x, y < 2^16) ----
91	
92	def w_succ(+one: Nat, +h1: {one == 1n : Nat}) -> {1n+Nat.sub(C.shift(16n, one), 1n) == C.shift(16n, one) : Nat}:
93	  N.sub_add(C.shift(16n, one), 1n, N.lt_succ_le_succ(0n, C.shift(16n, one), B.pos_pos(one, h1, 1n)))
94	
95	# x + 2^16 a = a W + x with W = 1 + wp
96	def digit_form(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +a: Nat) -> {Nat.add(x, C.shift(16n, a)) == Nat.add(Nat.mul(a, 1n+Nat.sub(C.shift(16n, one), 1n)), x) : Nat}:
97	  %Equal.sym(Nat, 1n+Nat.sub(C.shift(16n, one), 1n), C.shift(16n, one), w_succ(one, h1)) : {Nat.add(x, C.shift(16n, a)) == Nat.add(Nat.mul(a, _), x) : Nat}
98	  %Equal.sym(Nat, C.shift(16n, a), Nat.mul(a, C.shift(16n, one)), WW.shift_mul_one(16n, one, h1, a)) : {Nat.add(x, _) == Nat.add(Nat.mul(a, C.shift(16n, one)), x) : Nat}
99	  %Equal.sym(Nat, Nat.add(x, Nat.mul(a, C.shift(16n, one))), Nat.add(Nat.mul(a, C.shift(16n, one)), x), NA.add_comm(x, Nat.mul(a, C.shift(16n, one)))) : {_ == Nat.add(Nat.mul(a, C.shift(16n, one)), x) : Nat}
100	  {==}
101	
102	def lt_w(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}) -> {Nat.is_lt(x, 1n+Nat.sub(C.shift(16n, one), 1n)) == True{} : Bool}:
103	  %Equal.sym(Nat, 1n+Nat.sub(C.shift(16n, one), 1n), C.shift(16n, one), w_succ(one, h1)) : {Nat.is_lt(x, _) == True{} : Bool}
104	  hx
105	
106	def uniq_lo(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +y: Nat, +a: Nat, +b: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}, +hy: {Nat.is_lt(y, C.shift(16n, one)) == True{} : Bool}, +e: {Nat.add(x, C.shift(16n, a)) == Nat.add(y, C.shift(16n, b)) : Nat}) -> {x == y : Nat}:
107	  +wp = Nat.sub(C.shift(16n, one), 1n)
108	  +ex = Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(a, 1n+wp), x), 1n+wp), x, NR.mod_of(a, wp, x, lt_w(one, h1, x, hx)))
109	  +ey = NR.mod_of(b, wp, y, lt_w(one, h1, y, hy))
110	  +e2 = Equal.trans(Nat, Nat.add(Nat.mul(a, 1n+wp), x), Nat.add(x, C.shift(16n, a)), Nat.add(Nat.mul(b, 1n+wp), y), Equal.sym(Nat, Nat.add(x, C.shift(16n, a)), Nat.add(Nat.mul(a, 1n+wp), x), digit_form(one, h1, x, a)), Equal.trans(Nat, Nat.add(x, C.shift(16n, a)), Nat.add(y, C.shift(16n, b)), Nat.add(Nat.mul(b, 1n+wp), y), e, digit_form(one, h1, y, b)))
111	  Equal.trans(Nat, x, Nat.mod(Nat.add(Nat.mul(a, 1n+wp), x), 1n+wp), y, ex, Equal.trans(Nat, Nat.mod(Nat.add(Nat.mul(a, 1n+wp), x), 1n+wp), Nat.mod(Nat.add(Nat.mul(b, 1n+wp), y), 1n+wp), y, Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+wp), Nat.add(Nat.mul(a, 1n+wp), x), Nat.add(Nat.mul(b, 1n+wp), y), e2), ey))
112	
113	def uniq_hi(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +y: Nat, +a: Nat, +b: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}, +hy: {Nat.is_lt(y, C.shift(16n, one)) == True{} : Bool}, +e: {Nat.add(x, C.shift(16n, a)) == Nat.add(y, C.shift(16n, b)) : Nat}) -> {a == b : Nat}:
114	  +wp = Nat.sub(C.shift(16n, one), 1n)
115	  +ex = Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(a, 1n+wp), x), 1n+wp), a, NR.div_of(a, wp, x, lt_w(one, h1, x, hx)))
116	  +ey = NR.div_of(b, wp, y, lt_w(one, h1, y, hy))
117	  +e2 = Equal.trans(Nat, Nat.add(Nat.mul(a, 1n+wp), x), Nat.add(x, C.shift(16n, a)), Nat.add(Nat.mul(b, 1n+wp), y), Equal.sym(Nat, Nat.add(x, C.shift(16n, a)), Nat.add(Nat.mul(a, 1n+wp), x), digit_form(one, h1, x, a)), Equal.trans(Nat, Nat.add(x, C.shift(16n, a)), Nat.add(y, C.shift(16n, b)), Nat.add(Nat.mul(b, 1n+wp), y), e, digit_form(one, h1, y, b)))
118	  Equal.trans(Nat, a, Nat.div(Nat.add(Nat.mul(a, 1n+wp), x), 1n+wp), b, ex, Equal.trans(Nat, Nat.div(Nat.add(Nat.mul(a, 1n+wp), x), 1n+wp), Nat.div(Nat.add(Nat.mul(b, 1n+wp), y), 1n+wp), b, Equal.cong(Nat, Nat, z => Nat.div(z, 1n+wp), Nat.add(Nat.mul(a, 1n+wp), x), Nat.add(Nat.mul(b, 1n+wp), y), e2), ey))
119	
120	def eq_digit_f(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +y: Nat, +a: Nat, +b: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}, +hy: {Nat.is_lt(y, C.shift(16n, one)) == True{} : Bool}, +h: {Nat.is_eq(Nat.add(x, C.shift(16n, a)), Nat.add(y, C.shift(16n, b))) == True{} : Bool}) -> {Bool.and(Nat.is_eq(x, y), Nat.is_eq(a, b)) == True{} : Bool}:
121	  +e = N.eq_from_is_eq(Nat.add(x, C.shift(16n, a)), Nat.add(y, C.shift(16n, b)), h)
122	  +exy = uniq_lo(one, h1, x, y, a, b, hx, hy, e)
123	  +eab = uniq_hi(one, h1, x, y, a, b, hx, hy, e)
124	  Lg.and_intro(Nat.is_eq(x, y), Nat.is_eq(a, b), Lg.subst(Nat, z => {Nat.is_eq(x, z) == True{} : Bool}, x, y, exy, N.is_eq_refl(x)), Lg.subst(Nat, z => {Nat.is_eq(a, z) == True{} : Bool}, a, b, eab, N.is_eq_refl(a)))
125	
126	def eq_digit_g(+x: Nat, +y: Nat, +a: Nat, +b: Nat, +h: {Bool.and(Nat.is_eq(x, y), Nat.is_eq(a, b)) == True{} : Bool}) -> {Nat.is_eq(Nat.add(x, C.shift(16n, a)), Nat.add(y, C.shift(16n, b))) == True{} : Bool}:
127	  +exy = N.eq_from_is_eq(x, y, Lg.and_left(Nat.is_eq(x, y), Nat.is_eq(a, b), h))
128	  +eab = N.eq_from_is_eq(a, b, Lg.and_right(Nat.is_eq(x, y), Nat.is_eq(a, b), h))
129	  %Equal.sym(Nat, x, y, exy) : {Nat.is_eq(Nat.add(_, C.shift(16n, a)), Nat.add(y, C.shift(16n, b))) == True{} : Bool}
130	  %Equal.sym(Nat, a, b, eab) : {Nat.is_eq(Nat.add(y, C.shift(16n, _)), Nat.add(y, C.shift(16n, b))) == True{} : Bool}
131	  N.is_eq_refl(Nat.add(y, C.shift(16n, b)))
132	
133	def eq_digit(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +y: Nat, +a: Nat, +b: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}, +hy: {Nat.is_lt(y, C.shift(16n, one)) == True{} : Bool}) -> {Nat.is_eq(Nat.add(x, C.shift(16n, a)), Nat.add(y, C.shift(16n, b))) == Bool.and(Nat.is_eq(x, y), Nat.is_eq(a, b)) : Bool}:
134	  iff_bool(Nat.is_eq(Nat.add(x, C.shift(16n, a)), Nat.add(y, C.shift(16n, b))), Bool.and(Nat.is_eq(x, y), Nat.is_eq(a, b)), h => eq_digit_f(one, h1, x, y, a, b, hx, hy, h), h => eq_digit_g(x, y, a, b, h))
135	
136	# ---- eq ----
137	
138	# (x - y) + (y - x) == 0 exactly when x == y
139	def absdiff(x: Nat, y: Nat) -> {Nat.is_eq(Nat.add(Nat.sub(x, y), Nat.sub(y, x)), 0n) == Nat.is_eq(x, y) : Bool}:
140	  match x y:
141	    case 0n 0n:
142	      {==}
143	    case 0n 1n+q:
144	      {==}
145	    case 1n+p 0n:
146	      {==}
147	    case 1n+p 1n+q:
148	      absdiff(p, q)
149	
150	def diff_v(+one: Nat, +h1: {one == 1n : Nat}, n: Nat, xs: List<&2, Nat>, ys: List<&2, Nat>, +acc: Nat, +hx: {FS.limbs16(one, n, xs) == True{} : Bool}, +hy: {FS.limbs16(one, n, ys) == True{} : Bool}) -> {Nat.is_eq(L.diff(xs, ys, acc), 0n) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(LV.ev(xs), LV.ev(ys))) : Bool}:
151	  match n xs ys:
152	    case 0n Nil{} Nil{}:
153	      Equal.sym(Bool, Bool.and(Nat.is_eq(acc, 0n), True{}), Nat.is_eq(acc, 0n), and_true_r(Nat.is_eq(acc, 0n)))
154	    case 0n Nil{} y <> yt:
155	      Empty.absurd({Nat.is_eq(L.diff([], y <> yt, acc), 0n) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(LV.ev([]), LV.ev(y <> yt))) : Bool}, Lg.false_true(hy))
156	    case 0n x <> xt _:
157	      Empty.absurd({Nat.is_eq(L.diff(x <> xt, ys, acc), 0n) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(LV.ev(x <> xt), LV.ev(ys))) : Bool}, Lg.false_true(hx))
158	    case 1n+k Nil{} _:
159	      Empty.absurd({Nat.is_eq(L.diff([], ys, acc), 0n) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(LV.ev([]), LV.ev(ys))) : Bool}, Lg.false_true(hx))
160	    case 1n+k x <> xt Nil{}:
161	      Empty.absurd({Nat.is_eq(L.diff(x <> xt, [], acc), 0n) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(LV.ev(x <> xt), LV.ev([]))) : Bool}, Lg.false_true(hy))
162	    case 1n+ +k +x <> +xt +y <> +yt:
163	      +hx0 = Lg.and_left(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, xt), hx)
164	      +hy0 = Lg.and_left(Nat.is_lt(y, C.shift(16n, one)), FS.limbs16(one, k, yt), hy)
165	      +hxt = Lg.and_right(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, xt), hx)
166	      +hyt = Lg.and_right(Nat.is_lt(y, C.shift(16n, one)), FS.limbs16(one, k, yt), hy)
167	      %Equal.sym(Bool, Nat.is_eq(L.diff(xt, yt, Nat.add(acc, Nat.add(Nat.sub(x, y), Nat.sub(y, x)))), 0n), Bool.and(Nat.is_eq(Nat.add(acc, Nat.add(Nat.sub(x, y), Nat.sub(y, x))), 0n), Nat.is_eq(LV.ev(xt), LV.ev(yt))), diff_v(one, h1, k, xt, yt, Nat.add(acc, Nat.add(Nat.sub(x, y), Nat.sub(y, x))), hxt, hyt)) : {_ == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(xt))), Nat.add(y, C.shift(16n, LV.ev(yt))))) : Bool}
168	      %Equal.sym(Bool, Nat.is_eq(Nat.add(acc, Nat.add(Nat.sub(x, y), Nat.sub(y, x))), 0n), Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(Nat.add(Nat.sub(x, y), Nat.sub(y, x)), 0n)), is_eq_add0(acc, Nat.add(Nat.sub(x, y), Nat.sub(y, x)))) : {Bool.and(_, Nat.is_eq(LV.ev(xt), LV.ev(yt))) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(xt))), Nat.add(y, C.shift(16n, LV.ev(yt))))) : Bool}
169	      %Equal.sym(Bool, Nat.is_eq(Nat.add(Nat.sub(x, y), Nat.sub(y, x)), 0n), Nat.is_eq(x, y), absdiff(x, y)) : {Bool.and(Bool.and(Nat.is_eq(acc, 0n), _), Nat.is_eq(LV.ev(xt), LV.ev(yt))) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(xt))), Nat.add(y, C.shift(16n, LV.ev(yt))))) : Bool}
170	      %Equal.sym(Bool, Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(xt))), Nat.add(y, C.shift(16n, LV.ev(yt)))), Bool.and(Nat.is_eq(x, y), Nat.is_eq(LV.ev(xt), LV.ev(yt))), eq_digit(one, h1, x, y, LV.ev(xt), LV.ev(yt), hx0, hy0)) : {Bool.and(Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, y)), Nat.is_eq(LV.ev(xt), LV.ev(yt))) == Bool.and(Nat.is_eq(acc, 0n), _) : Bool}
171	      %Equal.sym(Bool, Bool.and(Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, y)), Nat.is_eq(LV.ev(xt), LV.ev(yt))), Bool.and(Nat.is_eq(acc, 0n), Bool.and(Nat.is_eq(x, y), Nat.is_eq(LV.ev(xt), LV.ev(yt)))), and_assoc(Nat.is_eq(acc, 0n), Nat.is_eq(x, y), Nat.is_eq(LV.ev(xt), LV.ev(yt)))) : {_ == Bool.and(Nat.is_eq(acc, 0n), Bool.and(Nat.is_eq(x, y), Nat.is_eq(LV.ev(xt), LV.ev(yt)))) : Bool}
172	      {==}
173	
174	def eq_v(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, Nat>, +ys: List<&2, Nat>, +hx: {FS.limbs16(one, 16n, xs) == True{} : Bool}, +hy: {FS.limbs16(one, 16n, ys) == True{} : Bool}) -> {L.eq(xs, ys) == Nat.is_eq(LV.ev(xs), LV.ev(ys)) : Bool}:
175	  diff_v(one, h1, 16n, xs, ys, 0n, hx, hy)
176	
177	# ---- x < m through the carry out of x + c ----
178	
179	def hz(+lo: Nat, hi: Nat, +t: Nat, +hl: {Nat.is_lt(lo, t) == True{} : Bool}) -> {Nat.is_eq(hi, 0n) == Nat.is_lt(Nat.add(lo, Nat.mul(hi, t)), t) : Bool}:
180	  match hi:
181	    case 0n:
182	      %Equal.sym(Nat, Nat.add(lo, 0n), lo, NA.add_zero(lo)) : {True{} == Nat.is_lt(_, t) : Bool}
183	      Equal.sym(Bool, Nat.is_lt(lo, t), True{}, hl)
184	    case 1n+ +k:
185	      Equal.sym(Bool, Nat.is_lt(Nat.add(lo, Nat.add(t, Nat.mul(k, t))), t), False{}, N.le_not_lt(Nat.add(lo, Nat.add(t, Nat.mul(k, t))), t, N.le_trans(t, Nat.add(t, Nat.mul(k, t)), Nat.add(lo, Nat.add(t, Nat.mul(k, t))), N.le_add_right(t, Nat.mul(k, t)), I.le_add_l(lo, Nat.add(t, Nat.mul(k, t))))))
186	
187	def ltm_v(+one: Nat, +h1: {one == 1n : Nat}, +mp: Nat, +c: List<&2, Nat>, +hm: {Nat.add(1n+mp, LV.ev(c)) == C.shift(256n, one) : Nat}, +x: List<&2, Nat>) -> {L.ltm(c, x) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}:
188	  +u = L.carry(32n, L.add(x, c), 0n)
189	  +hu16 = B.carry_limbs(one, h1, 32n, 16n, L.add(x, c), 0n, {==})
190	  +ll = I.lt_subst_r(LV.ev(L.take(16n, u)), LV.pos(16n, one), C.shift(256n, one), B.pos16(one), B.limbs_lt(one, h1, 16n, L.take(16n, u), hu16))
191	  %Equal.sym(Nat, L.horner(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), LV.horner_v(L.drop(16n, L.carry(32n, L.add(x, c), 0n)))) : {Nat.is_eq(_, 0n) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}
192	  %Equal.sym(Bool, Nat.is_eq(LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), 0n), Nat.is_lt(Nat.add(LV.ev(L.take(16n, L.carry(32n, L.add(x, c), 0n))), Nat.mul(LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), C.shift(256n, one))), C.shift(256n, one)), hz(LV.ev(L.take(16n, L.carry(32n, L.add(x, c), 0n))), LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), C.shift(256n, one), ll)) : {_ == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}
193	  %Equal.sym(Nat, Nat.add(LV.ev(L.take(16n, L.carry(32n, L.add(x, c), 0n))), Nat.mul(LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), C.shift(256n, one))), LV.ev(L.carry(32n, L.add(x, c), 0n)), Equal.sym(Nat, LV.ev(L.carry(32n, L.add(x, c), 0n)), Nat.add(LV.ev(L.take(16n, L.carry(32n, L.add(x, c), 0n))), Nat.mul(LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), C.shift(256n, one))), R.split256(one, h1, L.carry(32n, L.add(x, c), 0n)))) : {Nat.is_lt(_, C.shift(256n, one)) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}
194	  %Equal.sym(Nat, LV.ev(L.carry(32n, L.add(x, c), 0n)), Nat.add(LV.ev(x), LV.ev(c)), R.u_val(c, x)) : {Nat.is_lt(_, C.shift(256n, one)) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}
195	  %Equal.sym(Nat, C.shift(256n, one), Nat.add(1n+mp, LV.ev(c)), Equal.sym(Nat, Nat.add(1n+mp, LV.ev(c)), C.shift(256n, one), hm)) : {Nat.is_lt(Nat.add(LV.ev(x), LV.ev(c)), _) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}
196	  WW.lt_cancel_r(LV.ev(x), 1n+mp, LV.ev(c))
197	
198	def ltm_vv(+one: Nat, +h1: {one == 1n : Nat}, +mp: Nat, +c: List<&2, Nat>, +hm: {Nat.add(1n+mp, FS.value(one, c)) == C.shift(256n, one) : Nat}, +x: List<&2, Nat>) -> {L.ltm(c, x) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}:
199	  ltm_v(one, h1, mp, c, Lg.subst(Nat, z => {Nat.add(1n+mp, z) == C.shift(256n, one) : Nat}, FS.value(one, c), LV.ev(c), LV.ev_value(one, h1, c), hm), x)
200	
201	# ---- small constants: norm16([k]) for k < 2^16 ----
202	
203	def small_ev(+k: Nat) -> {LV.ev([k]) == k : Nat}:
204	  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(k, _) == k : Nat}
205	  %Equal.sym(Nat, Nat.add(k, 0n), k, NA.add_zero(k)) : {_ == k : Nat}
206	  {==}
207	
208	def small_v(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk: {Nat.is_lt(k, C.shift(256n, one)) == True{} : Bool}) -> {LV.ev(L.norm16([k])) == k : Nat}:
209	  +x = L.carry(32n, [k], 0n)
210	  +ex = Equal.trans(Nat, LV.ev(x), LV.ev([k]), k, LV.carry_v(32n, [k], 0n), small_ev(k))
211	  %Equal.sym(Nat, LV.ev(L.take(16n, L.carry(32n, [k], 0n))), LV.ev(L.carry(32n, [k], 0n)), R.take_small(one, h1, L.carry(32n, [k], 0n), I.lt_subst_l(k, LV.ev(x), C.shift(256n, one), Equal.sym(Nat, LV.ev(x), k, ex), hk))) : {_ == k : Nat}
212	  %Equal.sym(Nat, LV.ev(L.carry(32n, [k], 0n)), k, ex) : {_ == k : Nat}
213	  {==}
214	
215	def small_l(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat) -> {FS.limbs16(one, 16n, L.norm16([k])) == True{} : Bool}:
216	  B.carry_limbs(one, h1, 32n, 16n, [k], 0n, {==})