proofs/math/typed/width.bend

bend-collections-laws-crypto@1.0.0.0 · 467 lines · 60 definitions

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