proofs/math/typed/u32int.bend

bend-collections-laws-math@1.0.0.0 · 1,337 lines · 147 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as SG
4import bend-collections-laws-math@1.0.0.0/spec/math/natural.bend as NS
5import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as G
6import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM
7import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
8import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
9import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
10import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
11import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
12import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
13import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
14import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32.bend as U32P
15import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
16import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32mont.bend as MO
17import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
18import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF
19import bend-collections-laws-math@1.0.0.0/proofs/math/typed/combnat.bend as CN
20import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as AR2
21import bend-collections-laws-math@1.0.0.0/proofs/math/natural/fact.bend as FA
22import bend-collections-laws-math@1.0.0.0/proofs/math/natural/roots.bend as RT
23import bend-collections-laws-math@1.0.0.0/src/math/pow2.bend as P2
24import bend-collections-laws-math@1.0.0.0/proofs/math/pow2/pow2.bend as PP
25import bend-collections-laws-math@1.0.0.0/spec/math/natural.bend as S
26import bend-collections-laws-math@1.0.0.0/proofs/math/natural/inverse.bend as IV
27import bend-collections-laws-math@1.0.0.0/proofs/math/natural/proof.bend as NP
28
29# The integer clauses of spec/math/generic.bend at the U32 instance, proved
30# from the instance laws of spec/math/instances.bend (proofs/math/typed/
31# u32laws.bend): each generic function is simulated on the values and
32# compared with the proved Nat function of natural.bend, as Mathlib proves a
33# function on a type through its value (Mathlib's Fin / UInt32 lemmas via
34# toNat). The same text, read with the U64 laws, proves them at U64.
35
36def v(+x: U32) -> Nat:
37  SG.u32_val(x)
38
39def of(+n: Nat) -> U32:
40  SG.u32_of(n)
41
42# x is the U32 of its value
43def as_of(+x: U32, +n: Nat, +h: {v(x) == n : Nat}) -> {x == of(n) : U32}:
44  Equal.trans(U32, x, of(v(x)), of(n), Equal.sym(U32, of(v(x)), x, LW.rt(x)), Equal.cong(Nat, U32, t => of(t), v(x), n, h))
45
46def true_ne_false(+h: {True{} == False{} : Bool}) -> Empty:
47  U32P.true_ne_false(h)
48
49# ---- isqrt, abs ----
50
51def isqrt_agrees(+n: U32) -> SG.Isqrt.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, n):
52  as_of(I.u32_op(NM.Sqrt{n}), M.isqrt(v(n)), LW.ops_sqrt(n))
53
54def abs_identity(+x: U32) -> SG.Abs.identity(~U32, ~I.u32_op, ~I.u32_is, x):
55  LW.ops_abs(x)
56
57# ---- divmod ----
58
59def dm(+a: U32, +b: U32, +c: Bool, +hc: {I.u32_is(NM.IsZero{b}) == c : Bool}, +nb: Nat, +hnb: {v(b) == nb : Nat}) -> {G.divmod_ok(~U32, ~I.u32_op, a, b, c) == SG.lift_qr(~U32, ~SG.u32_of, M.divmod(v(a), nb)) : Result<&2, &2, NM.NumError, G.QuotRem<U32>>}:
60  match c nb:
61    case True{} 0n:
62      {==}
63    case False{} 0n:
64      +hz = Equal.trans(Bool, False{}, I.u32_is(NM.IsZero{b}), Nat.is_eq(0n, 0n), Equal.sym(Bool, I.u32_is(NM.IsZero{b}), False{}, hc), Equal.trans(Bool, I.u32_is(NM.IsZero{b}), Nat.is_eq(v(b), 0n), Nat.is_eq(0n, 0n), LW.tests_is_zero(b), Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(b), 0n, hnb)))
65      Empty.absurd({G.divmod_ok(~U32, ~I.u32_op, a, b, False{}) == SG.lift_qr(~U32, ~SG.u32_of, M.divmod(v(a), 0n)) : Result<&2, &2, NM.NumError, G.QuotRem<U32>>}, true_ne_false(Equal.sym(Bool, False{}, True{}, hz)))
66    case True{} 1n+ +bp:
67      +hz = Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{b}), Nat.is_eq(1n+bp, 0n), Equal.sym(Bool, I.u32_is(NM.IsZero{b}), True{}, hc), Equal.trans(Bool, I.u32_is(NM.IsZero{b}), Nat.is_eq(v(b), 0n), Nat.is_eq(1n+bp, 0n), LW.tests_is_zero(b), Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(b), 1n+bp, hnb)))
68      Empty.absurd({G.divmod_ok(~U32, ~I.u32_op, a, b, True{}) == SG.lift_qr(~U32, ~SG.u32_of, M.divmod(v(a), 1n+bp)) : Result<&2, &2, NM.NumError, G.QuotRem<U32>>}, true_ne_false(hz))
69    case False{} 1n+ +bp:
70      +hq = Equal.trans(Bool, Nat.is_eq(v(b), 0n), Nat.is_eq(1n+bp, 0n), False{}, Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(b), 1n+bp, hnb), {==})
71      +eq = as_of(I.u32_op(NM.Quot{a, b}), Nat.div(v(a), 1n+bp), Equal.trans(Nat, v(I.u32_op(NM.Quot{a, b})), Nat.div(v(a), v(b)), Nat.div(v(a), 1n+bp), LW.ops_quot(a, b, hq), Equal.cong(Nat, Nat, t => Nat.div(v(a), t), v(b), 1n+bp, hnb)))
72      +er = as_of(I.u32_op(NM.Rem{a, b}), Nat.mod(v(a), 1n+bp), Equal.trans(Nat, v(I.u32_op(NM.Rem{a, b})), Nat.mod(v(a), v(b)), Nat.mod(v(a), 1n+bp), LW.ops_rem(a, b, hq), Equal.cong(Nat, Nat, t => Nat.mod(v(a), t), v(b), 1n+bp, hnb)))
73      %Equal.sym(U32, I.u32_op(NM.Quot{a, b}), of(Nat.div(v(a), 1n+bp)), eq) : {Done{G.TQR{_, I.u32_op(NM.Rem{a, b})}} == Done{G.TQR{of(Nat.div(v(a), 1n+bp)), of(Nat.mod(v(a), 1n+bp))}} : Result<&2, &2, NM.NumError, G.QuotRem<U32>>}
74      %Equal.sym(U32, I.u32_op(NM.Rem{a, b}), of(Nat.mod(v(a), 1n+bp)), er) : {Done{G.TQR{of(Nat.div(v(a), 1n+bp)), _}} == Done{G.TQR{of(Nat.div(v(a), 1n+bp)), of(Nat.mod(v(a), 1n+bp))}} : Result<&2, &2, NM.NumError, G.QuotRem<U32>>}
75      {==}
76
77def divmod_agrees(+a: U32, +b: U32) -> SG.DivMod.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, a, b):
78  dm(a, b, I.u32_is(NM.IsZero{b}), {==}, v(b), {==})
79
80# ---- selections ----
81
82def lt_of(+a: U32, +b: U32, +c: Bool, +hc: {I.u32_is(NM.Lt{a, b}) == c : Bool}) -> {Nat.is_lt(v(a), v(b)) == c : Bool}:
83  Equal.trans(Bool, Nat.is_lt(v(a), v(b)), I.u32_is(NM.Lt{a, b}), c, Equal.sym(Bool, I.u32_is(NM.Lt{a, b}), Nat.is_lt(v(a), v(b)), LW.tests_lt(a, b)), hc)
84
85def min_c(+a: U32, +b: U32, +c: Bool, +hc: {I.u32_is(NM.Lt{b, a}) == c : Bool}) -> {G.pick(U32, c, b, a) == of(Nat.min(v(a), v(b))) : U32}:
86  match c:
87    case True{}:
88      as_of(b, Nat.min(v(a), v(b)), Equal.sym(Nat, Nat.min(v(a), v(b)), v(b), U32P.min_of_lt(v(a), v(b), lt_of(b, a, True{}, hc))))
89    case False{}:
90      as_of(a, Nat.min(v(a), v(b)), Equal.sym(Nat, Nat.min(v(a), v(b)), v(a), U32P.min_of_ge(v(a), v(b), lt_of(b, a, False{}, hc))))
91
92def min_agrees(+a: U32, +b: U32) -> SG.Min.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, a, b):
93  min_c(a, b, I.u32_is(NM.Lt{b, a}), {==})
94
95def max_c(+a: U32, +b: U32, +c: Bool, +hc: {I.u32_is(NM.Lt{a, b}) == c : Bool}) -> {G.pick(U32, c, b, a) == of(Nat.max(v(a), v(b))) : U32}:
96  match c:
97    case True{}:
98      as_of(b, Nat.max(v(a), v(b)), Equal.sym(Nat, Nat.max(v(a), v(b)), v(b), U32P.max_of_lt(v(a), v(b), lt_of(a, b, True{}, hc))))
99    case False{}:
100      as_of(a, Nat.max(v(a), v(b)), Equal.sym(Nat, Nat.max(v(a), v(b)), v(a), U32P.max_of_ge(v(a), v(b), lt_of(a, b, False{}, hc))))
101
102def max_agrees(+a: U32, +b: U32) -> SG.Max.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, a, b):
103  max_c(a, b, I.u32_is(NM.Lt{a, b}), {==})
104
105def max_val_c(+x: U32, +lo: U32, +c: Bool, +hc: {I.u32_is(NM.Lt{x, lo}) == c : Bool}) -> {v(G.pick(U32, c, lo, x)) == Nat.max(v(x), v(lo)) : Nat}:
106  match c:
107    case True{}:
108      Equal.sym(Nat, Nat.max(v(x), v(lo)), v(lo), U32P.max_of_lt(v(x), v(lo), lt_of(x, lo, True{}, hc)))
109    case False{}:
110      Equal.sym(Nat, Nat.max(v(x), v(lo)), v(x), U32P.max_of_ge(v(x), v(lo), lt_of(x, lo, False{}, hc)))
111
112def zero_v() -> {v(I.u32_op(NM.ZeroOp{})) == 0n : Nat}:
113  LW.ops_zero()
114
115def one_v() -> {v(I.u32_op(NM.One{})) == 1n : Nat}:
116  LW.ops_one()
117
118def sign_b(+x: U32, +c: Bool, +hc: {I.u32_is(NM.Lt{x, I.u32_op(NM.ZeroOp{})}) == c : Bool}, +hz: {Nat.is_lt(0n, v(x)) == False{} : Bool}) -> {G.sign_below(~U32, ~I.u32_op, ~I.u32_is, x, c) == of(Nat.min(v(x), 1n)) : U32}:
119  match c:
120    case True{}:
121      +hl = L.subst(Nat, z => {Nat.is_lt(v(x), z) == True{} : Bool}, v(I.u32_op(NM.ZeroOp{})), 0n, zero_v(), lt_of(x, I.u32_op(NM.ZeroOp{}), True{}, hc))
122      Empty.absurd({G.sign_below(~U32, ~I.u32_op, ~I.u32_is, x, True{}) == of(Nat.min(v(x), 1n)) : U32}, N.lt_zero_absurd(v(x), hl))
123    case False{}:
124      as_of(x, Nat.min(v(x), 1n), Equal.sym(Nat, Nat.min(v(x), 1n), v(x), N.min_left(v(x), 1n, U32P.zero_lt_one(v(x), hz))))
125
126def sign_a(+x: U32, +c: Bool, +hc: {I.u32_is(NM.Lt{I.u32_op(NM.ZeroOp{}), x}) == c : Bool}) -> {G.sign_above(~U32, ~I.u32_op, ~I.u32_is, x, c) == of(Nat.min(v(x), 1n)) : U32}:
127  match c:
128    case True{}:
129      +hl = L.subst(Nat, z => {Nat.is_lt(z, v(x)) == True{} : Bool}, v(I.u32_op(NM.ZeroOp{})), 0n, zero_v(), lt_of(I.u32_op(NM.ZeroOp{}), x, True{}, hc))
130      +em = N.min_right(v(x), 1n, U32P.pos_ge_one(v(x), hl))
131      Equal.trans(U32, I.u32_op(NM.One{}), of(1n), of(Nat.min(v(x), 1n)), as_of(I.u32_op(NM.One{}), 1n, one_v()), Equal.cong(Nat, U32, t => of(t), 1n, Nat.min(v(x), 1n), Equal.sym(Nat, Nat.min(v(x), 1n), 1n, em)))
132    case False{}:
133      +hl = L.subst(Nat, z => {Nat.is_lt(z, v(x)) == False{} : Bool}, v(I.u32_op(NM.ZeroOp{})), 0n, zero_v(), lt_of(I.u32_op(NM.ZeroOp{}), x, False{}, hc))
134      sign_b(x, I.u32_is(NM.Lt{x, I.u32_op(NM.ZeroOp{})}), {==}, hl)
135
136def sign_agrees(+x: U32) -> SG.Sign.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, x):
137  sign_a(x, I.u32_is(NM.Lt{I.u32_op(NM.ZeroOp{}), x}), {==})
138
139def clamp_d(+x: U32, +lo: U32, +hi: U32, +c: Bool) -> {G.clamp_ok(~U32, ~I.u32_op, ~I.u32_is, x, lo, hi, c) == SG.lift(~U32, ~SG.u32_of, M.clamp_ok(v(x), v(lo), v(hi), c)) : Result<&2, &2, NM.NumError, U32>}:
140  match c:
141    case True{}:
142      {==}
143    case False{}:
144      +m = G.max(~U32, ~I.u32_op, ~I.u32_is, x, lo)
145      +em = max_val_c(x, lo, I.u32_is(NM.Lt{x, lo}), {==})
146      %Equal.sym(U32, G.pick(U32, I.u32_is(NM.Lt{hi, m}), hi, m), of(Nat.min(v(m), v(hi))), min_c(m, hi, I.u32_is(NM.Lt{hi, m}), {==})) : {Done{_} == Done{of(Nat.min(Nat.max(v(x), v(lo)), v(hi)))} : Result<&2, &2, NM.NumError, U32>}
147      %Equal.sym(Nat, v(m), Nat.max(v(x), v(lo)), em) : {Done{of(Nat.min(_, v(hi)))} == Done{of(Nat.min(Nat.max(v(x), v(lo)), v(hi)))} : Result<&2, &2, NM.NumError, U32>}
148      {==}
149
150def clamp_c(+x: U32, +lo: U32, +hi: U32, +c: Bool, +hc: {I.u32_is(NM.Lt{hi, lo}) == c : Bool}) -> {G.clamp_ok(~U32, ~I.u32_op, ~I.u32_is, x, lo, hi, c) == SG.lift(~U32, ~SG.u32_of, M.clamp(v(x), v(lo), v(hi))) : Result<&2, &2, NM.NumError, U32>}:
151  %Equal.sym(Bool, Nat.is_lt(v(hi), v(lo)), c, lt_of(hi, lo, c, hc)) : {G.clamp_ok(~U32, ~I.u32_op, ~I.u32_is, x, lo, hi, c) == SG.lift(~U32, ~SG.u32_of, M.clamp_ok(v(x), v(lo), v(hi), _)) : Result<&2, &2, NM.NumError, U32>}
152  clamp_d(x, lo, hi, c)
153
154def clamp_agrees(+x: U32, +lo: U32, +hi: U32) -> SG.Clamp.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, x, lo, hi):
155  clamp_c(x, lo, hi, I.u32_is(NM.Lt{hi, lo}), {==})
156
157# ---- gcd: Euclid on the values, then enough fuel ----
158
159def gcd_sim(+f: Nat, +a: U32, +b: U32, +cz: Bool, +nb: Nat, +hcz: {I.u32_is(NM.IsZero{b}) == cz : Bool}, +hnb: {v(b) == nb : Nat}) -> {v(G.gcd_go(~U32, ~I.u32_op, ~I.u32_is, f, a, (b, cz))) == M.gcd_go(f, v(a), nb) : Nat}:
160  match f cz nb:
161    case 0n _ _:
162      {==}
163    case 1n+g True{} 0n:
164      {==}
165    case 1n+g True{} 1n+bp:
166      +hz = Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{b}), Nat.is_eq(1n+bp, 0n), Equal.sym(Bool, I.u32_is(NM.IsZero{b}), True{}, hcz), Equal.trans(Bool, I.u32_is(NM.IsZero{b}), Nat.is_eq(v(b), 0n), Nat.is_eq(1n+bp, 0n), LW.tests_is_zero(b), Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(b), 1n+bp, hnb)))
167      Empty.absurd({v(G.gcd_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, a, (b, True{}))) == M.gcd_go(1n+g, v(a), 1n+bp) : Nat}, true_ne_false(hz))
168    case 1n+g False{} 0n:
169      +hz = Equal.trans(Bool, False{}, I.u32_is(NM.IsZero{b}), Nat.is_eq(0n, 0n), Equal.sym(Bool, I.u32_is(NM.IsZero{b}), False{}, hcz), Equal.trans(Bool, I.u32_is(NM.IsZero{b}), Nat.is_eq(v(b), 0n), Nat.is_eq(0n, 0n), LW.tests_is_zero(b), Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(b), 0n, hnb)))
170      Empty.absurd({v(G.gcd_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, a, (b, False{}))) == M.gcd_go(1n+g, v(a), 0n) : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, hz)))
171    case 1n+ +g False{} 1n+ +bp:
172      +rm = I.u32_op(NM.Rem{a, b})
173      +hq = Equal.trans(Bool, Nat.is_eq(v(b), 0n), Nat.is_eq(1n+bp, 0n), False{}, Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(b), 1n+bp, hnb), {==})
174      +erm = Equal.trans(Nat, v(rm), Nat.mod(v(a), v(b)), Nat.mod(v(a), 1n+bp), LW.ops_rem(a, b, hq), Equal.cong(Nat, Nat, t => Nat.mod(v(a), t), v(b), 1n+bp, hnb))
175      +ih = gcd_sim(g, b, rm, I.u32_is(NM.IsZero{rm}), v(rm), {==}, {==})
176      Equal.trans(Nat, v(G.gcd_go(~U32, ~I.u32_op, ~I.u32_is, g, b, (rm, I.u32_is(NM.IsZero{rm})))), M.gcd_go(g, v(b), v(rm)), M.gcd_go(g, 1n+bp, Nat.mod(v(a), 1n+bp)), ih, Equal.trans(Nat, M.gcd_go(g, v(b), v(rm)), M.gcd_go(g, 1n+bp, v(rm)), M.gcd_go(g, 1n+bp, Nat.mod(v(a), 1n+bp)), Equal.cong(Nat, Nat, t => M.gcd_go(g, t, v(rm)), v(b), 1n+bp, hnb), Equal.cong(Nat, Nat, t => M.gcd_go(g, 1n+bp, t), v(rm), Nat.mod(v(a), 1n+bp), erm)))
177
178def gcd_val_k(+k: Nat, +hk: {k == 32n : Nat}, +a: U32, +b: U32) -> {v(G.gcd(~U32, ~I.u32_op, ~I.u32_is, a, b)) == M.gcd(v(a), v(b)) : Nat}:
179  +hk2 = L.subst(Nat, z => {Nat.is_le(1n+Nat.double(z), 140n) == True{} : Bool}, 32n, k, Equal.sym(Nat, k, 32n, hk), {==})
180  Equal.trans(Nat, v(G.gcd(~U32, ~I.u32_op, ~I.u32_is, a, b)), M.gcd_go(140n, v(a), v(b)), M.gcd(v(a), v(b)), gcd_sim(140n, a, b, I.u32_is(NM.IsZero{b}), v(b), {==}, {==}), NF.gcd_140(k, v(a), v(b), hk2, U32P.val_lt(1n, {==}, k, hk, b)))
181
182def gcd_val(+a: U32, +b: U32) -> {v(G.gcd(~U32, ~I.u32_op, ~I.u32_is, a, b)) == M.gcd(v(a), v(b)) : Nat}:
183  gcd_val_k(32n, {==}, a, b)
184
185def gcd_agrees(+a: U32, +b: U32) -> SG.Gcd.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, a, b):
186  as_of(G.gcd(~U32, ~I.u32_op, ~I.u32_is, a, b), M.gcd(v(a), v(b)), gcd_val(a, b))
187
188# ---- gcd_all: the fold on values ----
189
190def vals(xs: List<&2, U32>) -> List<&2, Nat>:
191  SG.vals(~U32, ~SG.u32_val, xs)
192
193def gall(+xs: List<&2, U32>, +acc: U32) -> {v(G.gcd_all_go(~U32, ~I.u32_op, ~I.u32_is, xs, acc)) == M.gcd_all_go(vals(xs), v(acc)) : Nat}:
194  match xs:
195    case Nil{}:
196      {==}
197    case Con{+x, +t}:
198      +g = G.gcd(~U32, ~I.u32_op, ~I.u32_is, acc, x)
199      Equal.trans(Nat, v(G.gcd_all_go(~U32, ~I.u32_op, ~I.u32_is, t, g)), M.gcd_all_go(vals(t), v(g)), M.gcd_all_go(vals(t), M.gcd(v(acc), v(x))), gall(t, g), Equal.cong(Nat, Nat, z => M.gcd_all_go(vals(t), z), v(g), M.gcd(v(acc), v(x)), gcd_val(acc, x)))
200
201def gcd_all_agrees(+xs: List<&2, U32>) -> SG.GcdAll.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, xs):
202  +z = I.u32_op(NM.ZeroOp{})
203  as_of(G.gcd_all(~U32, ~I.u32_op, ~I.u32_is, xs), M.gcd_all(vals(xs)), Equal.trans(Nat, v(G.gcd_all_go(~U32, ~I.u32_op, ~I.u32_is, xs, z)), M.gcd_all_go(vals(xs), v(z)), M.gcd_all_go(vals(xs), 0n), gall(xs, z), Equal.cong(Nat, Nat, t => M.gcd_all_go(vals(xs), t), v(z), 0n, zero_v())))
204
205# ---- a checked product ----
206
207def mo_of(+q: U32, +b: U32, +n: Nat, +hn: {Nat.mul(v(q), v(b)) == n : Nat}, +c: Bool, +hc: {C.fits(32n, n) == c : Bool}) -> {I.u32_is(NM.MulOver{q, b}) == Bool.not(c) : Bool}:
208  +e1 = Equal.trans(Bool, I.u32_is(NM.MulOver{q, b}), Bool.not(C.fits(32n, Nat.mul(v(q), v(b)))), Bool.not(C.fits(32n, n)), LW.tests_mul_over(q, b), Equal.cong(Nat, Bool, t => Bool.not(C.fits(32n, t)), Nat.mul(v(q), v(b)), n, hn))
209  Equal.trans(Bool, I.u32_is(NM.MulOver{q, b}), Bool.not(C.fits(32n, n)), Bool.not(c), e1, Equal.cong(Bool, Bool, t => Bool.not(t), C.fits(32n, n), c, hc))
210
211def cm(+q: U32, +b: U32, +n: Nat, +hn: {Nat.mul(v(q), v(b)) == n : Nat}, +c: Bool, +hc: {C.fits(32n, n) == c : Bool}) -> {G.ok(U32, G.cmul(~U32, ~I.u32_op, ~I.u32_is, q, b)) == SG.checked(~U32, ~SG.u32_of, 32n, n) : Result<&2, &2, NM.NumError, U32>}:
212  match c:
213    case True{}:
214      +hmo2 = mo_of(q, b, n, hn, True{}, hc)
215      %Equal.sym(Bool, I.u32_is(NM.MulOver{q, b}), False{}, hmo2) : {G.ok(U32, G.fits(U32, _, I.u32_op(NM.Mul{q, b}))) == SG.checked(~U32, ~SG.u32_of, 32n, n) : Result<&2, &2, NM.NumError, U32>}
216      %Equal.sym(Bool, C.fits(32n, n), True{}, hc) : {Done{I.u32_op(NM.Mul{q, b})} == SG.checked_pick(~U32, ~SG.u32_of, n, _) : Result<&2, &2, NM.NumError, U32>}
217      %Equal.sym(U32, I.u32_op(NM.Mul{q, b}), of(n), as_of(I.u32_op(NM.Mul{q, b}), n, Equal.trans(Nat, v(I.u32_op(NM.Mul{q, b})), Nat.mul(v(q), v(b)), n, LW.ops_mul(q, b, hmo2), hn))) : {Done{_} == Done{of(n)} : Result<&2, &2, NM.NumError, U32>}
218      {==}
219    case False{}:
220      +hmo = mo_of(q, b, n, hn, False{}, hc)
221      %Equal.sym(Bool, I.u32_is(NM.MulOver{q, b}), True{}, hmo) : {G.ok(U32, G.fits(U32, _, I.u32_op(NM.Mul{q, b}))) == SG.checked(~U32, ~SG.u32_of, 32n, n) : Result<&2, &2, NM.NumError, U32>}
222      %Equal.sym(Bool, C.fits(32n, n), False{}, hc) : {Fail{NM.Overflow{}} == SG.checked_pick(~U32, ~SG.u32_of, n, _) : Result<&2, &2, NM.NumError, U32>}
223      {==}
224
225# ---- lcm ----
226
227def gpos_d(+ap: Nat, +b: Nat, d: NS.dvd(M.gcd(1n+ap, b), 1n+ap), +g: Nat, +hg: {M.gcd(1n+ap, b) == g : Nat}) -> {Nat.is_eq(M.gcd(1n+ap, b), 0n) == False{} : Bool}:
228  (k, e) = d
229  match g:
230    case 0n:
231      +e0 = Equal.trans(Nat, 1n+ap, Nat.mul(k, M.gcd(1n+ap, b)), 0n, e, Equal.trans(Nat, Nat.mul(k, M.gcd(1n+ap, b)), Nat.mul(k, 0n), 0n, Equal.cong(Nat, Nat, t => Nat.mul(k, t), M.gcd(1n+ap, b), 0n, hg), NA.mul_zero(k)))
232      Empty.absurd({Nat.is_eq(M.gcd(1n+ap, b), 0n) == False{} : Bool}, N.succ_zero(ap, e0))
233    case 1n+gp:
234      %Equal.sym(Nat, M.gcd(1n+ap, b), 1n+gp, hg) : {Nat.is_eq(_, 0n) == False{} : Bool}
235      {==}
236
237# gcd of a positive number is positive
238def gpos(+ap: Nat, +b: Nat) -> {Nat.is_eq(M.gcd(1n+ap, b), 0n) == False{} : Bool}:
239  gpos_d(ap, b, NP.divides_left(1n+ap, b), M.gcd(1n+ap, b), {==})
240
241def iz(+a: U32, +n: Nat, +h: {v(a) == n : Nat}) -> {I.u32_is(NM.IsZero{a}) == Nat.is_eq(n, 0n) : Bool}:
242  Equal.trans(Bool, I.u32_is(NM.IsZero{a}), Nat.is_eq(v(a), 0n), Nat.is_eq(n, 0n), LW.tests_is_zero(a), Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(a), n, h))
243
244def lcmc(+a: U32, +b: U32, +c: Bool, +na: Nat, +nb: Nat, +hc: {Bool.or(I.u32_is(NM.IsZero{a}), I.u32_is(NM.IsZero{b})) == c : Bool}, +hna: {v(a) == na : Nat}, +hnb: {v(b) == nb : Nat}) -> {G.lcm_ok(~U32, ~I.u32_op, ~I.u32_is, a, b, c) == SG.checked(~U32, ~SG.u32_of, 32n, M.lcm(na, nb)) : Result<&2, &2, NM.NumError, U32>}:
245  match c na nb:
246    case True{} 0n _:
247      Equal.cong(U32, Result<&2, &2, NM.NumError, U32>, t => Done{t}, I.u32_op(NM.ZeroOp{}), of(0n), as_of(I.u32_op(NM.ZeroOp{}), 0n, zero_v()))
248    case True{} 1n+ap 0n:
249      Equal.cong(U32, Result<&2, &2, NM.NumError, U32>, t => Done{t}, I.u32_op(NM.ZeroOp{}), of(0n), as_of(I.u32_op(NM.ZeroOp{}), 0n, zero_v()))
250    case True{} 1n+ +ap 1n+ +bp:
251      Empty.absurd({G.lcm_ok(~U32, ~I.u32_op, ~I.u32_is, a, b, True{}) == SG.checked(~U32, ~SG.u32_of, 32n, M.lcm(1n+ap, 1n+bp)) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(Equal.trans(Bool, True{}, Bool.or(False{}, I.u32_is(NM.IsZero{b})), False{}, Equal.sym(Bool, Bool.or(False{}, I.u32_is(NM.IsZero{b})), True{}, L.subst(Bool, t => {Bool.or(t, I.u32_is(NM.IsZero{b})) == True{} : Bool}, I.u32_is(NM.IsZero{a}), False{}, iz(a, 1n+ap, hna), hc)), iz(b, 1n+bp, hnb))))
252    case False{} 0n _:
253      Empty.absurd({G.lcm_ok(~U32, ~I.u32_op, ~I.u32_is, a, b, False{}) == SG.checked(~U32, ~SG.u32_of, 32n, M.lcm(0n, nb)) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(Equal.trans(Bool, True{}, Bool.or(True{}, I.u32_is(NM.IsZero{b})), False{}, {==}, L.subst(Bool, t => {Bool.or(t, I.u32_is(NM.IsZero{b})) == False{} : Bool}, I.u32_is(NM.IsZero{a}), True{}, iz(a, 0n, hna), hc))))
254    case False{} 1n+ +ap 0n:
255      +h2 = L.subst(Bool, t => {Bool.or(t, I.u32_is(NM.IsZero{b})) == False{} : Bool}, I.u32_is(NM.IsZero{a}), False{}, iz(a, 1n+ap, hna), hc)
256      Empty.absurd({G.lcm_ok(~U32, ~I.u32_op, ~I.u32_is, a, b, False{}) == SG.checked(~U32, ~SG.u32_of, 32n, M.lcm(1n+ap, 0n)) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{b}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{b}), True{}, iz(b, 0n, hnb)), h2)))
257    case False{} 1n+ +ap 1n+ +bp:
258      +g = G.gcd(~U32, ~I.u32_op, ~I.u32_is, a, b)
259      +gg = M.gcd(1n+ap, 1n+bp)
260      +eg = Equal.trans(Nat, v(g), M.gcd(v(a), v(b)), gg, gcd_val(a, b), Equal.trans(Nat, M.gcd(v(a), v(b)), M.gcd(1n+ap, v(b)), gg, Equal.cong(Nat, Nat, t => M.gcd(t, v(b)), v(a), 1n+ap, hna), Equal.cong(Nat, Nat, t => M.gcd(1n+ap, t), v(b), 1n+bp, hnb)))
261      +hgz = L.subst(Nat, t => {Nat.is_eq(t, 0n) == False{} : Bool}, gg, v(g), Equal.sym(Nat, v(g), gg, eg), gpos(ap, 1n+bp))
262      +q = I.u32_op(NM.Quot{a, g})
263      +eq = Equal.trans(Nat, v(q), Nat.div(v(a), v(g)), Nat.div(1n+ap, gg), LW.ops_quot(a, g, hgz), Equal.trans(Nat, Nat.div(v(a), v(g)), Nat.div(1n+ap, v(g)), Nat.div(1n+ap, gg), Equal.cong(Nat, Nat, t => Nat.div(t, v(g)), v(a), 1n+ap, hna), Equal.cong(Nat, Nat, t => Nat.div(1n+ap, t), v(g), gg, eg)))
264      +n = Nat.mul(Nat.div(1n+ap, gg), 1n+bp)
265      +hn = Equal.trans(Nat, Nat.mul(v(q), v(b)), Nat.mul(Nat.div(1n+ap, gg), v(b)), n, Equal.cong(Nat, Nat, t => Nat.mul(t, v(b)), v(q), Nat.div(1n+ap, gg), eq), Equal.cong(Nat, Nat, t => Nat.mul(Nat.div(1n+ap, gg), t), v(b), 1n+bp, hnb))
266      cm(q, b, n, hn, C.fits(32n, n), {==})
267
268def lcm_checked(+a: U32, +b: U32) -> SG.Lcm.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, a, b):
269  lcmc(a, b, Bool.or(I.u32_is(NM.IsZero{a}), I.u32_is(NM.IsZero{b})), v(a), v(b), {==}, {==}, {==})
270
271# ---- lcm_all: the fold stops at the first overflow ----
272
273def lall_fail(xs: List<&2, U32>, +e: NM.NumError) -> {G.lcm_all_go(~U32, ~I.u32_op, ~I.u32_is, xs, Fail{e}) == Fail{e} : Result<&2, &2, NM.NumError, U32>}:
274  match xs:
275    case Nil{}:
276      {==}
277    case Con{x, t}:
278      {==}
279
280def lgo_false(xs: List<&2, Nat>, +acc: Nat) -> {SG.lcm_go(32n, xs, acc, False{}) == (acc, False{}) : Nat & Bool}:
281  match xs:
282    case Nil{}:
283      {==}
284    case Con{x, t}:
285      {==}
286
287# the fold on an accumulator r == checked(n) (c == fits(32, n))
288def lall(+xs: List<&2, U32>, +r: Result<&2, &2, NM.NumError, U32>, +n: Nat, +c: Bool, +hr: {r == SG.checked_pick(~U32, ~SG.u32_of, n, c) : Result<&2, &2, NM.NumError, U32>}, +hc: {C.fits(32n, n) == c : Bool}) -> {G.lcm_all_go(~U32, ~I.u32_op, ~I.u32_is, xs, r) == SG.prefix_fin(~U32, ~SG.u32_of, SG.lcm_go(32n, vals(xs), n, c)) : Result<&2, &2, NM.NumError, U32>}:
289  match xs c:
290    case Nil{} _:
291      hr
292    case Con{x, t} False{}:
293      %Equal.sym(Result<&2, &2, NM.NumError, U32>, r, Fail{NM.Overflow{}}, hr) : {G.lcm_all_go(~U32, ~I.u32_op, ~I.u32_is, Con{x, t}, _) == Fail{NM.Overflow{}} : Result<&2, &2, NM.NumError, U32>}
294      {==}
295    case Con{+x, +t} True{}:
296      %Equal.sym(Result<&2, &2, NM.NumError, U32>, r, Done{of(n)}, hr) : {G.lcm_all_go(~U32, ~I.u32_op, ~I.u32_is, Con{x, t}, _) == SG.prefix_fin(~U32, ~SG.u32_of, SG.lcm_go(32n, vals(t), M.lcm(n, v(x)), C.fits(32n, M.lcm(n, v(x))))) : Result<&2, &2, NM.NumError, U32>}
297      +en = LW.vo(n, hc)
298      +el = Equal.trans(Result<&2, &2, NM.NumError, U32>, G.lcm(~U32, ~I.u32_op, ~I.u32_is, of(n), x), SG.checked(~U32, ~SG.u32_of, 32n, M.lcm(v(of(n)), v(x))), SG.checked(~U32, ~SG.u32_of, 32n, M.lcm(n, v(x))), lcm_checked(of(n), x), Equal.cong(Nat, Result<&2, &2, NM.NumError, U32>, z => SG.checked(~U32, ~SG.u32_of, 32n, M.lcm(z, v(x))), v(of(n)), n, en))
299      lall(t, G.lcm(~U32, ~I.u32_op, ~I.u32_is, of(n), x), M.lcm(n, v(x)), C.fits(32n, M.lcm(n, v(x))), el, {==})
300
301def lcm_all_checked(+xs: List<&2, U32>) -> SG.LcmAll.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, xs):
302  lall(xs, Done{I.u32_op(NM.One{})}, 1n, True{}, Equal.cong(U32, Result<&2, &2, NM.NumError, U32>, t => Done{t}, I.u32_op(NM.One{}), of(1n), as_of(I.u32_op(NM.One{}), 1n, one_v())), {==})
303
304# ---- prod: the fold stops at the first overflow ----
305
306def cmul_rel(+q: U32, +x: U32, +n: Nat, +hn: {Nat.mul(v(q), v(x)) == n : Nat}, +c: Bool, +hc: {C.fits(32n, n) == c : Bool}) -> {G.cmul(~U32, ~I.u32_op, ~I.u32_is, q, x) == G.fits(U32, Bool.not(c), of(n)) : Maybe<&2, U32>}:
307  match c:
308    case True{}:
309      +hmo = mo_of(q, x, n, hn, True{}, hc)
310      %Equal.sym(Bool, I.u32_is(NM.MulOver{q, x}), False{}, hmo) : {G.fits(U32, _, I.u32_op(NM.Mul{q, x})) == Some{of(n)} : Maybe<&2, U32>}
311      Equal.cong(U32, Maybe<&2, U32>, t => Some{t}, I.u32_op(NM.Mul{q, x}), of(n), as_of(I.u32_op(NM.Mul{q, x}), n, Equal.trans(Nat, v(I.u32_op(NM.Mul{q, x})), Nat.mul(v(q), v(x)), n, LW.ops_mul(q, x, hmo), hn)))
312    case False{}:
313      %Equal.sym(Bool, I.u32_is(NM.MulOver{q, x}), True{}, mo_of(q, x, n, hn, False{}, hc)) : {G.fits(U32, _, I.u32_op(NM.Mul{q, x})) == None{} : Maybe<&2, U32>}
314      {==}
315
316def pal(+xs: List<&2, U32>, +r: Maybe<&2, U32>, +n: Nat, +c: Bool, +hr: {r == G.fits(U32, Bool.not(c), of(n)) : Maybe<&2, U32>}, +hc: {C.fits(32n, n) == c : Bool}) -> {G.ok(U32, G.prod_go(~U32, ~I.u32_op, ~I.u32_is, xs, r)) == SG.prefix_fin(~U32, ~SG.u32_of, SG.prod_go(32n, vals(xs), n, c)) : Result<&2, &2, NM.NumError, U32>}:
317  match xs c:
318    case Nil{} True{}:
319      %Equal.sym(Maybe<&2, U32>, r, Some{of(n)}, hr) : {G.ok(U32, _) == Done{of(n)} : Result<&2, &2, NM.NumError, U32>}
320      {==}
321    case Nil{} False{}:
322      %Equal.sym(Maybe<&2, U32>, r, None{}, hr) : {G.ok(U32, _) == Fail{NM.Overflow{}} : Result<&2, &2, NM.NumError, U32>}
323      {==}
324    case Con{x, t} False{}:
325      %Equal.sym(Maybe<&2, U32>, r, None{}, hr) : {G.ok(U32, G.prod_go(~U32, ~I.u32_op, ~I.u32_is, Con{x, t}, _)) == Fail{NM.Overflow{}} : Result<&2, &2, NM.NumError, U32>}
326      {==}
327    case Con{+x, +t} True{}:
328      %Equal.sym(Maybe<&2, U32>, r, Some{of(n)}, hr) : {G.ok(U32, G.prod_go(~U32, ~I.u32_op, ~I.u32_is, Con{x, t}, _)) == SG.prefix_fin(~U32, ~SG.u32_of, SG.prod_go(32n, vals(t), Nat.mul(n, v(x)), C.fits(32n, Nat.mul(n, v(x))))) : Result<&2, &2, NM.NumError, U32>}
329      +hn = Equal.cong(Nat, Nat, z => Nat.mul(z, v(x)), v(of(n)), n, LW.vo(n, hc))
330      pal(t, G.cmul(~U32, ~I.u32_op, ~I.u32_is, of(n), x), Nat.mul(n, v(x)), C.fits(32n, Nat.mul(n, v(x))), cmul_rel(of(n), x, Nat.mul(n, v(x)), hn, C.fits(32n, Nat.mul(n, v(x))), {==}), {==})
331
332def prod_checked(+xs: List<&2, U32>) -> SG.Prod.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, xs):
333  pal(xs, Some{I.u32_op(NM.One{})}, 1n, True{}, Equal.cong(U32, Maybe<&2, U32>, t => Some{t}, I.u32_op(NM.One{}), of(1n), as_of(I.u32_op(NM.One{}), 1n, one_v())), {==})
334
335# ---- sum: the partial sums only grow ----
336
337def ao_of(+q: U32, +b: U32, +n: Nat, +hn: {Nat.add(v(q), v(b)) == n : Nat}, +c: Bool, +hc: {C.fits(32n, n) == c : Bool}) -> {I.u32_is(NM.AddOver{q, b}) == Bool.not(c) : Bool}:
338  +e1 = Equal.trans(Bool, I.u32_is(NM.AddOver{q, b}), Bool.not(C.fits(32n, Nat.add(v(q), v(b)))), Bool.not(C.fits(32n, n)), LW.tests_add_over(q, b), Equal.cong(Nat, Bool, t => Bool.not(C.fits(32n, t)), Nat.add(v(q), v(b)), n, hn))
339  Equal.trans(Bool, I.u32_is(NM.AddOver{q, b}), Bool.not(C.fits(32n, n)), Bool.not(c), e1, Equal.cong(Bool, Bool, t => Bool.not(t), C.fits(32n, n), c, hc))
340
341def cadd_rel(+q: U32, +x: U32, +n: Nat, +hn: {Nat.add(v(q), v(x)) == n : Nat}, +c: Bool, +hc: {C.fits(32n, n) == c : Bool}) -> {G.cadd(~U32, ~I.u32_op, ~I.u32_is, q, x) == G.fits(U32, Bool.not(c), of(n)) : Maybe<&2, U32>}:
342  match c:
343    case True{}:
344      +hao = ao_of(q, x, n, hn, True{}, hc)
345      %Equal.sym(Bool, I.u32_is(NM.AddOver{q, x}), False{}, hao) : {G.fits(U32, _, I.u32_op(NM.Add{q, x})) == Some{of(n)} : Maybe<&2, U32>}
346      Equal.cong(U32, Maybe<&2, U32>, t => Some{t}, I.u32_op(NM.Add{q, x}), of(n), as_of(I.u32_op(NM.Add{q, x}), n, Equal.trans(Nat, v(I.u32_op(NM.Add{q, x})), Nat.add(v(q), v(x)), n, LW.ops_add(q, x, hao), hn)))
347    case False{}:
348      %Equal.sym(Bool, I.u32_is(NM.AddOver{q, x}), True{}, ao_of(q, x, n, hn, False{}, hc)) : {G.fits(U32, _, I.u32_op(NM.Add{q, x})) == None{} : Maybe<&2, U32>}
349      {==}
350
351# a value that does not fit stays unfit when it grows
352def unfit_mono(+k: Nat, +a: Nat, +b: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}, +hf: {C.fits(k, a) == False{} : Bool}) -> {C.fits(k, b) == False{} : Bool}:
353  +na = Equal.trans(Bool, Nat.is_lt(a, C.pow2(k)), C.fits(k, a), False{}, Equal.sym(Bool, C.fits(k, a), Nat.is_lt(a, C.pow2(k)), WW.fits_lt(k, a)), hf)
354  Equal.trans(Bool, C.fits(k, b), Nat.is_lt(b, C.pow2(k)), False{}, WW.fits_lt(k, b), N.le_not_lt(b, C.pow2(k), N.le_trans(C.pow2(k), a, b, N.not_lt_le(a, C.pow2(k), na), h)))
355
356def sal(+xs: List<&2, U32>, +r: Maybe<&2, U32>, +n: Nat, +c: Bool, +hr: {r == G.fits(U32, Bool.not(c), of(n)) : Maybe<&2, U32>}, +hc: {C.fits(32n, n) == c : Bool}) -> {G.ok(U32, G.sum_go(~U32, ~I.u32_op, ~I.u32_is, xs, r)) == SG.checked(~U32, ~SG.u32_of, 32n, Nat.add(n, NS.lsum(vals(xs)))) : Result<&2, &2, NM.NumError, U32>}:
357  match xs c:
358    case Nil{} True{}:
359      %Equal.sym(Maybe<&2, U32>, r, Some{of(n)}, hr) : {G.ok(U32, _) == SG.checked(~U32, ~SG.u32_of, 32n, Nat.add(n, 0n)) : Result<&2, &2, NM.NumError, U32>}
360      %Equal.sym(Nat, Nat.add(n, 0n), n, N.add_zero(n)) : {Done{of(n)} == SG.checked(~U32, ~SG.u32_of, 32n, _) : Result<&2, &2, NM.NumError, U32>}
361      %Equal.sym(Bool, C.fits(32n, n), True{}, hc) : {Done{of(n)} == SG.checked_pick(~U32, ~SG.u32_of, n, _) : Result<&2, &2, NM.NumError, U32>}
362      {==}
363    case Nil{} False{}:
364      %Equal.sym(Maybe<&2, U32>, r, None{}, hr) : {G.ok(U32, _) == SG.checked(~U32, ~SG.u32_of, 32n, Nat.add(n, 0n)) : Result<&2, &2, NM.NumError, U32>}
365      %Equal.sym(Nat, Nat.add(n, 0n), n, N.add_zero(n)) : {Fail{NM.Overflow{}} == SG.checked(~U32, ~SG.u32_of, 32n, _) : Result<&2, &2, NM.NumError, U32>}
366      %Equal.sym(Bool, C.fits(32n, n), False{}, hc) : {Fail{NM.Overflow{}} == SG.checked_pick(~U32, ~SG.u32_of, n, _) : Result<&2, &2, NM.NumError, U32>}
367      {==}
368    case Con{x, t} False{}:
369      %Equal.sym(Maybe<&2, U32>, r, None{}, hr) : {G.ok(U32, G.sum_go(~U32, ~I.u32_op, ~I.u32_is, Con{x, t}, _)) == SG.checked(~U32, ~SG.u32_of, 32n, Nat.add(n, NS.lsum(vals(Con{x, t})))) : Result<&2, &2, NM.NumError, U32>}
370      +s = Nat.add(n, NS.lsum(vals(Con{x, t})))
371      %Equal.sym(Bool, C.fits(32n, s), False{}, unfit_mono(32n, n, s, N.le_add_right(n, NS.lsum(vals(Con{x, t}))), hc)) : {Fail{NM.Overflow{}} == SG.checked_pick(~U32, ~SG.u32_of, s, _) : Result<&2, &2, NM.NumError, U32>}
372      {==}
373    case Con{+x, +t} True{}:
374      +n2 = Nat.add(n, v(x))
375      +hn = Equal.cong(Nat, Nat, z => Nat.add(z, v(x)), v(of(n)), n, LW.vo(n, hc))
376      %Equal.sym(Maybe<&2, U32>, r, Some{of(n)}, hr) : {G.ok(U32, G.sum_go(~U32, ~I.u32_op, ~I.u32_is, Con{x, t}, _)) == SG.checked(~U32, ~SG.u32_of, 32n, Nat.add(n, Nat.add(v(x), NS.lsum(vals(t))))) : Result<&2, &2, NM.NumError, U32>}
377      %NA.add_assoc(n, v(x), NS.lsum(vals(t))) : {G.ok(U32, G.sum_go(~U32, ~I.u32_op, ~I.u32_is, t, G.cadd(~U32, ~I.u32_op, ~I.u32_is, of(n), x))) == SG.checked(~U32, ~SG.u32_of, 32n, _) : Result<&2, &2, NM.NumError, U32>}
378      sal(t, G.cadd(~U32, ~I.u32_op, ~I.u32_is, of(n), x), n2, C.fits(32n, n2), cadd_rel(of(n), x, n2, hn, C.fits(32n, n2), {==}), {==})
379
380def sum_checked(+xs: List<&2, U32>) -> SG.Sum.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, xs):
381  sal(xs, Some{I.u32_op(NM.ZeroOp{})}, 0n, True{}, Equal.cong(U32, Maybe<&2, U32>, t => Some{t}, I.u32_op(NM.ZeroOp{}), of(0n), as_of(I.u32_op(NM.ZeroOp{}), 0n, zero_v())), {==})
382
383# ---- bit_length: halvings on the values ----
384
385def blsim(+f: Nat, +k: Nat, +n: U32, +cz: Bool, +nn: Nat, +hcz: {I.u32_is(NM.IsZero{n}) == cz : Bool}, +hnn: {v(n) == nn : Nat}) -> {G.bit_length_go(~U32, ~I.u32_op, ~I.u32_is, f, k, (n, cz)) == M.bit_length_go(f, nn, k) : Nat}:
386  match f cz nn:
387    case 0n _ _:
388      {==}
389    case 1n+g True{} 0n:
390      {==}
391    case 1n+g True{} 1n+np:
392      Empty.absurd({G.bit_length_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, k, (n, True{})) == M.bit_length_go(1n+g, 1n+np, k) : Nat}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{n}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{n}), True{}, hcz), iz(n, 1n+np, hnn))))
393    case 1n+g False{} 0n:
394      Empty.absurd({G.bit_length_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, k, (n, False{})) == M.bit_length_go(1n+g, 0n, k) : Nat}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{n}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{n}), True{}, iz(n, 0n, hnn)), hcz)))
395    case 1n+ +g False{} 1n+ +np:
396      +h = I.u32_op(NM.Half{n})
397      +eh = Equal.trans(Nat, v(h), Nat.div(v(n), 2n), Nat.div(1n+np, 2n), LW.ops_half(n), Equal.cong(Nat, Nat, t => Nat.div(t, 2n), v(n), 1n+np, hnn))
398      blsim(g, 1n+k, h, I.u32_is(NM.IsZero{h}), Nat.div(1n+np, 2n), {==}, eh)
399
400def bit_length_k(+k: Nat, +hk: {k == 32n : Nat}, +n: U32) -> {G.bit_length(~U32, ~I.u32_op, ~I.u32_is, n) == M.bit_length(v(n)) : Nat}:
401  +hj = L.subst(Nat, z => {Nat.is_le(z, 140n) == True{} : Bool}, 32n, k, Equal.sym(Nat, k, 32n, hk), {==})
402  Equal.trans(Nat, G.bit_length(~U32, ~I.u32_op, ~I.u32_is, n), M.bit_length_go(140n, v(n), 0n), M.bit_length(v(n)), blsim(140n, 0n, n, I.u32_is(NM.IsZero{n}), v(n), {==}, {==}), NF.bl_140(k, v(n), hj, U32P.val_lt(1n, {==}, k, hk, n)))
403
404def bit_length_agrees(+n: U32) -> SG.BitLength.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, n):
405  bit_length_k(32n, {==}, n)
406
407# ---- pow_mod: binary exponentiation on the values, below m ----
408
409def pmo_lt(+mp: Nat, +d: Nat, +base: Nat, +acc: Nat, +ha: {Nat.is_lt(acc, 1n+mp) == True{} : Bool}) -> {Nat.is_lt(M.pow_mod_odd(1n+mp, d, base, acc), 1n+mp) == True{} : Bool}:
410  match d:
411    case 0n:
412      ha
413    case 1n+z:
414      NR.dm_lt(mp, Nat.mul(acc, base))
415
416def lt_m(+x: U32, +m: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}, +h: {Nat.is_lt(v(x), 1n+mp) == True{} : Bool}) -> {Nat.is_lt(v(x), v(m)) == True{} : Bool}:
417  L.subst(Nat, z => {Nat.is_lt(v(x), z) == True{} : Bool}, 1n+mp, v(m), Equal.sym(Nat, v(m), 1n+mp, hm), h)
418
419def mmb_v(+m: U32, +b: U32, +acc: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}, +hb: {Nat.is_lt(v(b), 1n+mp) == True{} : Bool}, +ha: {Nat.is_lt(v(acc), 1n+mp) == True{} : Bool}, +d: Nat, +o: Bool, +hd: {Nat.is_lt(d, 2n) == True{} : Bool}, +ho: {o == Nat.is_eq(d, 1n) : Bool}) -> {v(G.mm_bit(~U32, ~I.u32_op, o, m, b, acc)) == M.pow_mod_odd(1n+mp, d, v(b), v(acc)) : Nat}:
420  match d o:
421    case 0n False{}:
422      {==}
423    case 0n True{}:
424      Empty.absurd({v(G.mm_bit(~U32, ~I.u32_op, True{}, m, b, acc)) == M.pow_mod_odd(1n+mp, 0n, v(b), v(acc)) : Nat}, true_ne_false(ho))
425    case 1n True{}:
426      Equal.trans(Nat, v(I.u32_op(NM.MulMod{acc, b, m})), Nat.mod(Nat.mul(v(acc), v(b)), v(m)), Nat.mod(Nat.mul(v(acc), v(b)), 1n+mp), LW.ops_mulmod(acc, b, m, lt_m(acc, m, mp, hm, ha), lt_m(b, m, mp, hm, hb)), Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(v(acc), v(b)), t), v(m), 1n+mp, hm))
427    case 1n False{}:
428      Empty.absurd({v(G.mm_bit(~U32, ~I.u32_op, False{}, m, b, acc)) == M.pow_mod_odd(1n+mp, 1n, v(b), v(acc)) : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, ho)))
429    case 2n+q _:
430      Empty.absurd({v(G.mm_bit(~U32, ~I.u32_op, o, m, b, acc)) == M.pow_mod_odd(1n+mp, 2n+q, v(b), v(acc)) : Nat}, N.lt_zero_absurd(q, hd))
431
432def pmsim(+f: Nat, +m: U32, +b: U32, +acc: U32, +e: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}, +hb: {Nat.is_lt(v(b), 1n+mp) == True{} : Bool}, +ha: {Nat.is_lt(v(acc), 1n+mp) == True{} : Bool}, +ez: Bool, +ne: Nat, +hez: {I.u32_is(NM.IsZero{e}) == ez : Bool}, +hne: {v(e) == ne : Nat}) -> {v(G.pow_mod_go(~U32, ~I.u32_op, ~I.u32_is, f, m, b, acc, (e, ez))) == M.pow_mod_go(f, 1n+mp, ne, v(b), v(acc)) : Nat}:
433  match f ez ne:
434    case 0n _ _:
435      {==}
436    case 1n+g True{} 0n:
437      {==}
438    case 1n+g True{} 1n+ep:
439      Empty.absurd({v(G.pow_mod_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, m, b, acc, (e, True{}))) == M.pow_mod_go(1n+g, 1n+mp, 1n+ep, v(b), v(acc)) : Nat}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{e}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{e}), True{}, hez), iz(e, 1n+ep, hne))))
440    case 1n+g False{} 0n:
441      Empty.absurd({v(G.pow_mod_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, m, b, acc, (e, False{}))) == M.pow_mod_go(1n+g, 1n+mp, 0n, v(b), v(acc)) : Nat}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{e}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{e}), True{}, iz(e, 0n, hne)), hez)))
442    case 1n+ +g False{} 1n+ +ep:
443      +b2 = I.u32_op(NM.MulMod{b, b, m})
444      +eb2 = Equal.trans(Nat, v(b2), Nat.mod(Nat.mul(v(b), v(b)), v(m)), Nat.mod(Nat.mul(v(b), v(b)), 1n+mp), LW.ops_mulmod(b, b, m, lt_m(b, m, mp, hm, hb), lt_m(b, m, mp, hm, hb)), Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(v(b), v(b)), t), v(m), 1n+mp, hm))
445      +hb2 = L.subst(Nat, z => {Nat.is_lt(z, 1n+mp) == True{} : Bool}, Nat.mod(Nat.mul(v(b), v(b)), 1n+mp), v(b2), Equal.sym(Nat, v(b2), Nat.mod(Nat.mul(v(b), v(b)), 1n+mp), eb2), NR.dm_lt(mp, Nat.mul(v(b), v(b))))
446      +o = I.u32_is(NM.Odd{e})
447      +d = Nat.mod(1n+ep, 2n)
448      +ho = Equal.trans(Bool, o, Nat.is_eq(Nat.mod(v(e), 2n), 1n), Nat.is_eq(d, 1n), LW.tests_odd(e), Equal.cong(Nat, Bool, t => Nat.is_eq(Nat.mod(t, 2n), 1n), v(e), 1n+ep, hne))
449      +acc2 = G.mm_bit(~U32, ~I.u32_op, o, m, b, acc)
450      +ea2 = mmb_v(m, b, acc, mp, hm, hb, ha, d, o, NR.dm_lt(1n, 1n+ep), ho)
451      +ha2 = L.subst(Nat, z => {Nat.is_lt(z, 1n+mp) == True{} : Bool}, M.pow_mod_odd(1n+mp, d, v(b), v(acc)), v(acc2), Equal.sym(Nat, v(acc2), M.pow_mod_odd(1n+mp, d, v(b), v(acc)), ea2), pmo_lt(mp, d, v(b), v(acc), ha))
452      +e2 = I.u32_op(NM.Half{e})
453      +ee2 = Equal.trans(Nat, v(e2), Nat.div(v(e), 2n), Nat.div(1n+ep, 2n), LW.ops_half(e), Equal.cong(Nat, Nat, t => Nat.div(t, 2n), v(e), 1n+ep, hne))
454      +ih = pmsim(g, m, b2, acc2, e2, mp, hm, hb2, ha2, I.u32_is(NM.IsZero{e2}), Nat.div(1n+ep, 2n), {==}, ee2)
455      Equal.trans(Nat, v(G.pow_mod_go(~U32, ~I.u32_op, ~I.u32_is, g, m, b2, acc2, (e2, I.u32_is(NM.IsZero{e2})))), M.pow_mod_go(g, 1n+mp, Nat.div(1n+ep, 2n), v(b2), v(acc2)), M.pow_mod_go(g, 1n+mp, Nat.div(1n+ep, 2n), Nat.mod(Nat.mul(v(b), v(b)), 1n+mp), M.pow_mod_odd(1n+mp, d, v(b), v(acc))), ih, Equal.trans(Nat, M.pow_mod_go(g, 1n+mp, Nat.div(1n+ep, 2n), v(b2), v(acc2)), M.pow_mod_go(g, 1n+mp, Nat.div(1n+ep, 2n), Nat.mod(Nat.mul(v(b), v(b)), 1n+mp), v(acc2)), M.pow_mod_go(g, 1n+mp, Nat.div(1n+ep, 2n), Nat.mod(Nat.mul(v(b), v(b)), 1n+mp), M.pow_mod_odd(1n+mp, d, v(b), v(acc))), Equal.cong(Nat, Nat, t => M.pow_mod_go(g, 1n+mp, Nat.div(1n+ep, 2n), t, v(acc2)), v(b2), Nat.mod(Nat.mul(v(b), v(b)), 1n+mp), eb2), Equal.cong(Nat, Nat, t => M.pow_mod_go(g, 1n+mp, Nat.div(1n+ep, 2n), Nat.mod(Nat.mul(v(b), v(b)), 1n+mp), t), v(acc2), M.pow_mod_odd(1n+mp, d, v(b), v(acc)), ea2)))
456
457def pm_rem(+x: U32, +m: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}) -> {v(I.u32_op(NM.Rem{x, m})) == Nat.mod(v(x), 1n+mp) : Nat}:
458  +hq = Equal.trans(Bool, Nat.is_eq(v(m), 0n), Nat.is_eq(1n+mp, 0n), False{}, Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(m), 1n+mp, hm), {==})
459  Equal.trans(Nat, v(I.u32_op(NM.Rem{x, m})), Nat.mod(v(x), v(m)), Nat.mod(v(x), 1n+mp), LW.ops_rem(x, m, hq), Equal.cong(Nat, Nat, t => Nat.mod(v(x), t), v(m), 1n+mp, hm))
460
461
462# the generic MulMod loop (mont32_ok(m) False)
463def pm_gen(+k: Nat, +hk: {k == 32n : Nat}, +b: U32, +e: U32, +m: U32, +mp: Nat, +hnm: {v(m) == 1n+mp : Nat}) -> {v(G.pow_mod_go(~U32, ~I.u32_op, ~I.u32_is, 140n, m, I.u32_op(NM.Rem{b, m}), I.u32_op(NM.Rem{I.u32_op(NM.One{}), m}), (e, I.u32_is(NM.IsZero{e})))) == M.pow_mod_go(v(e), 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp)) : Nat}:
464  +rb = I.u32_op(NM.Rem{b, m})
465  +ra = I.u32_op(NM.Rem{I.u32_op(NM.One{}), m})
466  +eb = pm_rem(b, m, mp, hnm)
467  +ea = Equal.trans(Nat, v(ra), Nat.mod(v(I.u32_op(NM.One{})), 1n+mp), Nat.mod(1n, 1n+mp), pm_rem(I.u32_op(NM.One{}), m, mp, hnm), Equal.cong(Nat, Nat, t => Nat.mod(t, 1n+mp), v(I.u32_op(NM.One{})), 1n, one_v()))
468  +hb = L.subst(Nat, z => {Nat.is_lt(z, 1n+mp) == True{} : Bool}, Nat.mod(v(b), 1n+mp), v(rb), Equal.sym(Nat, v(rb), Nat.mod(v(b), 1n+mp), eb), NR.dm_lt(mp, v(b)))
469  +ha = L.subst(Nat, z => {Nat.is_lt(z, 1n+mp) == True{} : Bool}, Nat.mod(1n, 1n+mp), v(ra), Equal.sym(Nat, v(ra), Nat.mod(1n, 1n+mp), ea), NR.dm_lt(mp, 1n))
470  +hj = L.subst(Nat, z => {Nat.is_le(z, 140n) == True{} : Bool}, 32n, k, Equal.sym(Nat, k, 32n, hk), {==})
471  +s = pmsim(140n, m, rb, ra, e, mp, hnm, hb, ha, I.u32_is(NM.IsZero{e}), v(e), {==}, {==})
472  +c1 = Equal.trans(Nat, M.pow_mod_go(140n, 1n+mp, v(e), v(rb), v(ra)), M.pow_mod_go(140n, 1n+mp, v(e), Nat.mod(v(b), 1n+mp), v(ra)), M.pow_mod_go(140n, 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp)), Equal.cong(Nat, Nat, t => M.pow_mod_go(140n, 1n+mp, v(e), t, v(ra)), v(rb), Nat.mod(v(b), 1n+mp), eb), Equal.cong(Nat, Nat, t => M.pow_mod_go(140n, 1n+mp, v(e), Nat.mod(v(b), 1n+mp), t), v(ra), Nat.mod(1n, 1n+mp), ea))
473  +c2 = NF.pm_140(k, 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp), hj, U32P.val_lt(1n, {==}, k, hk, e))
474  Equal.trans(Nat, v(G.pow_mod_go(~U32, ~I.u32_op, ~I.u32_is, 140n, m, I.u32_op(NM.Rem{b, m}), I.u32_op(NM.Rem{I.u32_op(NM.One{}), m}), (e, I.u32_is(NM.IsZero{e})))), M.pow_mod_go(140n, 1n+mp, v(e), v(rb), v(ra)), M.pow_mod_go(v(e), 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp)), s, Equal.trans(Nat, M.pow_mod_go(140n, 1n+mp, v(e), v(rb), v(ra)), M.pow_mod_go(140n, 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp)), M.pow_mod_go(v(e), 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp)), c1, c2))
475
476# 32-bit Montgomery multiplication (mont32_ok(m) True)
477def pm_mont(+k: Nat, +hk: {k == 32n : Nat}, +b: U32, +e: U32, +m: U32, +mp: Nat, +hnm: {v(m) == 1n+mp : Nat}, +hok: {X.mont32_ok(m) == True{} : Bool}) -> {v(I.u32_op(NM.PowMod{I.u32_op(NM.Rem{b, m}), e, m})) == M.pow_mod_go(v(e), 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp)) : Nat}:
478  +hj = L.subst(Nat, z => {Nat.is_le(z, 140n) == True{} : Bool}, 32n, k, Equal.sym(Nat, k, 32n, hk), {==})
479  Equal.trans(Nat, v(X.mpow32(U32.mod(b, m), e, m)), M.pow_mod_go(140n, 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp)), M.pow_mod_go(v(e), 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp)), MO.mpow_top(1n, {==}, mp, m, hnm, hok, b, e), NF.pm_140(k, 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp), hj, U32P.val_lt(1n, {==}, k, hk, e)))
480
481def pm_pick(+k: Nat, +hk: {k == 32n : Nat}, +b: U32, +e: U32, +m: U32, +mp: Nat, +hnm: {v(m) == 1n+mp : Nat}, +c: Bool, +hc: {X.mont32_ok(m) == c : Bool}) -> {v(G.pow_mod_pick(~U32, ~I.u32_op, ~I.u32_is, b, e, m, c)) == M.pow_mod_go(v(e), 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp)) : Nat}:
482  match c:
483    case True{}:
484      pm_mont(k, hk, b, e, m, mp, hnm, hc)
485    case False{}:
486      pm_gen(k, hk, b, e, m, mp, hnm)
487
488def pm_top(+k: Nat, +hk: {k == 32n : Nat}, +b: U32, +e: U32, +m: U32, +c: Bool, +hc: {I.u32_is(NM.IsZero{m}) == c : Bool}, +nm: Nat, +hnm: {v(m) == nm : Nat}) -> {G.pow_mod_ok(~U32, ~I.u32_op, ~I.u32_is, b, e, m, c) == SG.lift(~U32, ~SG.u32_of, M.pow_mod(v(b), v(e), nm)) : Result<&2, &2, NM.NumError, U32>}:
489  match c nm:
490    case True{} 0n:
491      {==}
492    case False{} 0n:
493      Empty.absurd({G.pow_mod_ok(~U32, ~I.u32_op, ~I.u32_is, b, e, m, False{}) == SG.lift(~U32, ~SG.u32_of, M.pow_mod(v(b), v(e), 0n)) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{m}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{m}), True{}, iz(m, 0n, hnm)), hc)))
494    case True{} 1n+ +mp:
495      Empty.absurd({G.pow_mod_ok(~U32, ~I.u32_op, ~I.u32_is, b, e, m, True{}) == SG.lift(~U32, ~SG.u32_of, M.pow_mod(v(b), v(e), 1n+mp)) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{m}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{m}), True{}, hc), iz(m, 1n+mp, hnm))))
496    case False{} 1n+ +mp:
497      +g = G.pow_mod_pick(~U32, ~I.u32_op, ~I.u32_is, b, e, m, I.u32_is(NM.Mont{m}))
498      +r = M.pow_mod_go(v(e), 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp))
499      Equal.cong(U32, Result<&2, &2, NM.NumError, U32>, t => Done{t}, g, of(r), as_of(g, r, pm_pick(k, hk, b, e, m, mp, hnm, X.mont32_ok(m), {==})))
500
501def powmod_agrees(+b: U32, +e: U32, +m: U32) -> SG.PowMod.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, b, e, m):
502  pm_top(32n, {==}, b, e, m, I.u32_is(NM.IsZero{m}), {==}, v(m), {==})
503
504# ---- mod_inverse: extended Euclid on the values, coefficients below m ----
505
506def nlt(+a: Nat, +b: Nat, +na: Nat, +nb: Nat, +ha: {a == na : Nat}, +hb: {b == nb : Nat}) -> {Nat.is_lt(a, b) == Nat.is_lt(na, nb) : Bool}:
507  Equal.trans(Bool, Nat.is_lt(a, b), Nat.is_lt(na, b), Nat.is_lt(na, nb), Equal.cong(Nat, Bool, t => Nat.is_lt(t, b), a, na, ha), Equal.cong(Nat, Bool, t => Nat.is_lt(na, t), b, nb, hb))
508
509def ltv(+a: U32, +b: U32, +na: Nat, +nb: Nat, +ha: {v(a) == na : Nat}, +hb: {v(b) == nb : Nat}) -> {I.u32_is(NM.Lt{a, b}) == Nat.is_lt(na, nb) : Bool}:
510  Equal.trans(Bool, I.u32_is(NM.Lt{a, b}), Nat.is_lt(v(a), v(b)), Nat.is_lt(na, nb), LW.tests_lt(a, b), nlt(v(a), v(b), na, nb, ha, hb))
511
512def nsub(+a: Nat, +b: Nat, +na: Nat, +nb: Nat, +ha: {a == na : Nat}, +hb: {b == nb : Nat}) -> {Nat.sub(a, b) == Nat.sub(na, nb) : Nat}:
513  Equal.trans(Nat, Nat.sub(a, b), Nat.sub(na, b), Nat.sub(na, nb), Equal.cong(Nat, Nat, t => Nat.sub(t, b), a, na, ha), Equal.cong(Nat, Nat, t => Nat.sub(na, t), b, nb, hb))
514
515def nadd(+a: Nat, +b: Nat, +na: Nat, +nb: Nat, +ha: {a == na : Nat}, +hb: {b == nb : Nat}) -> {Nat.add(a, b) == Nat.add(na, nb) : Nat}:
516  Equal.trans(Nat, Nat.add(a, b), Nat.add(na, b), Nat.add(na, nb), Equal.cong(Nat, Nat, t => Nat.add(t, b), a, na, ha), Equal.cong(Nat, Nat, t => Nat.add(na, t), b, nb, hb))
517
518def mv(+k: Nat, +hk: {k == 32n : Nat}, +m: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}) -> {Nat.is_lt(1n+mp, C.pow2(k)) == True{} : Bool}:
519  L.subst(Nat, z => {Nat.is_lt(z, C.pow2(k)) == True{} : Bool}, v(m), 1n+mp, hm, U32P.val_lt(1n, {==}, k, hk, m))
520
521def fits32(+k: Nat, +hk: {k == 32n : Nat}, +n: Nat, +h: {Nat.is_lt(n, C.pow2(k)) == True{} : Bool}) -> {C.fits(32n, n) == True{} : Bool}:
522  L.subst(Nat, z => {C.fits(z, n) == True{} : Bool}, k, 32n, hk, Equal.trans(Bool, C.fits(k, n), Nat.is_lt(n, C.pow2(k)), True{}, WW.fits_lt(k, n), h))
523
524def lt_mn(+x: U32, +m: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}, +nx: Nat, +hx: {v(x) == nx : Nat}, +h: {Nat.is_lt(nx, 1n+mp) == True{} : Bool}) -> {Nat.is_lt(v(x), v(m)) == True{} : Bool}:
525  lt_m(x, m, mp, hm, L.subst(Nat, z => {Nat.is_lt(z, 1n+mp) == True{} : Bool}, nx, v(x), Equal.sym(Nat, v(x), nx, hx), h))
526
527def subv(+k: Nat, +hk: {k == 32n : Nat}, +m: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}, +s0: U32, +x: U32, +ns0: Nat, +nx: Nat, +hs0: {v(s0) == ns0 : Nat}, +hx: {v(x) == nx : Nat}, +hb0: {Nat.is_lt(ns0, 1n+mp) == True{} : Bool}, +hbx: {Nat.is_lt(nx, 1n+mp) == True{} : Bool}, +c: Bool, +hc: {I.u32_is(NM.Lt{s0, x}) == c : Bool}) -> {v(G.submod(~U32, ~I.u32_op, m, s0, x, c)) == Nat.mod(Nat.add(ns0, Nat.sub(1n+mp, nx)), 1n+mp) : Nat}:
528  match c:
529    case True{}:
530      +hl = Equal.trans(Bool, Nat.is_lt(ns0, nx), I.u32_is(NM.Lt{s0, x}), True{}, Equal.sym(Bool, I.u32_is(NM.Lt{s0, x}), Nat.is_lt(ns0, nx), ltv(s0, x, ns0, nx, hs0, hx)), hc)
531      +y = I.u32_op(NM.Sub{m, x})
532      +ey = Equal.trans(Nat, v(y), Nat.sub(v(m), v(x)), Nat.sub(1n+mp, nx), LW.ops_sub(m, x, N.lt_le(v(x), v(m), lt_mn(x, m, mp, hm, nx, hx, hbx))), nsub(v(m), v(x), 1n+mp, nx, hm, hx))
533      +sum = Nat.add(ns0, Nat.sub(1n+mp, nx))
534      +hsum = NF.sm_lt(1n+mp, ns0, nx, hl, N.lt_le(nx, 1n+mp, hbx))
535      +esum = nadd(v(s0), v(y), ns0, Nat.sub(1n+mp, nx), hs0, ey)
536      +hfit = fits32(k, hk, Nat.add(v(s0), v(y)), L.subst(Nat, z => {Nat.is_lt(z, C.pow2(k)) == True{} : Bool}, sum, Nat.add(v(s0), v(y)), Equal.sym(Nat, Nat.add(v(s0), v(y)), sum, esum), N.lt_trans(sum, 1n+mp, C.pow2(k), hsum, mv(k, hk, m, mp, hm))))
537      +hao = Equal.trans(Bool, I.u32_is(NM.AddOver{s0, y}), Bool.not(C.fits(32n, Nat.add(v(s0), v(y)))), False{}, LW.tests_add_over(s0, y), Equal.cong(Bool, Bool, t => Bool.not(t), C.fits(32n, Nat.add(v(s0), v(y))), True{}, hfit))
538      Equal.trans(Nat, v(I.u32_op(NM.Add{s0, y})), Nat.add(v(s0), v(y)), Nat.mod(sum, 1n+mp), LW.ops_add(s0, y, hao), Equal.trans(Nat, Nat.add(v(s0), v(y)), sum, Nat.mod(sum, 1n+mp), esum, Equal.sym(Nat, Nat.mod(sum, 1n+mp), sum, NF.mod_small(mp, sum, hsum))))
539    case False{}:
540      +hl = Equal.trans(Bool, Nat.is_lt(ns0, nx), I.u32_is(NM.Lt{s0, x}), False{}, Equal.sym(Bool, I.u32_is(NM.Lt{s0, x}), Nat.is_lt(ns0, nx), ltv(s0, x, ns0, nx, hs0, hx)), hc)
541      +hlv = Equal.trans(Bool, Nat.is_lt(v(s0), v(x)), I.u32_is(NM.Lt{s0, x}), False{}, Equal.sym(Bool, I.u32_is(NM.Lt{s0, x}), Nat.is_lt(v(s0), v(x)), LW.tests_lt(s0, x)), hc)
542      Equal.trans(Nat, v(I.u32_op(NM.Sub{s0, x})), Nat.sub(v(s0), v(x)), Nat.mod(Nat.add(ns0, Nat.sub(1n+mp, nx)), 1n+mp), LW.ops_sub(s0, x, N.not_lt_le(v(s0), v(x), hlv)), Equal.trans(Nat, Nat.sub(v(s0), v(x)), Nat.sub(ns0, nx), Nat.mod(Nat.add(ns0, Nat.sub(1n+mp, nx)), 1n+mp), nsub(v(s0), v(x), ns0, nx, hs0, hx), Equal.sym(Nat, Nat.mod(Nat.add(ns0, Nat.sub(1n+mp, nx)), 1n+mp), Nat.sub(ns0, nx), NF.sm_ge(mp, ns0, nx, N.not_lt_le(ns0, nx, hl), hb0))))
543
544def stepv(+k: Nat, +hk: {k == 32n : Nat}, +m: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}, +q: U32, +s0: U32, +s1: U32, +nq: Nat, +ns0: Nat, +ns1: Nat, +hq: {v(q) == nq : Nat}, +hs0: {v(s0) == ns0 : Nat}, +hs1: {v(s1) == ns1 : Nat}, +hb0: {Nat.is_lt(ns0, 1n+mp) == True{} : Bool}, +hb1: {Nat.is_lt(ns1, 1n+mp) == True{} : Bool}) -> {v(G.inv_step(~U32, ~I.u32_op, ~I.u32_is, m, q, s0, s1)) == M.inv_step(1n+mp, nq, ns0, ns1) : Nat}:
545  +rq = I.u32_op(NM.Rem{q, m})
546  +erq = Equal.trans(Nat, v(rq), Nat.mod(v(q), 1n+mp), Nat.mod(nq, 1n+mp), pm_rem(q, m, mp, hm), Equal.cong(Nat, Nat, t => Nat.mod(t, 1n+mp), v(q), nq, hq))
547  +x = I.u32_op(NM.MulMod{rq, s1, m})
548  e1 = LW.ops_mulmod(rq, s1, m, lt_mn(rq, m, mp, hm, Nat.mod(nq, 1n+mp), erq, NR.dm_lt(mp, nq)), lt_mn(s1, m, mp, hm, ns1, hs1, hb1))
549  +e2 = Equal.trans(Nat, Nat.mod(Nat.mul(v(rq), v(s1)), v(m)), Nat.mod(Nat.mul(v(rq), v(s1)), 1n+mp), Nat.mod(Nat.mul(Nat.mod(nq, 1n+mp), ns1), 1n+mp), Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(v(rq), v(s1)), t), v(m), 1n+mp, hm), Equal.trans(Nat, Nat.mod(Nat.mul(v(rq), v(s1)), 1n+mp), Nat.mod(Nat.mul(Nat.mod(nq, 1n+mp), v(s1)), 1n+mp), Nat.mod(Nat.mul(Nat.mod(nq, 1n+mp), ns1), 1n+mp), Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(t, v(s1)), 1n+mp), v(rq), Nat.mod(nq, 1n+mp), erq), Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(Nat.mod(nq, 1n+mp), t), 1n+mp), v(s1), ns1, hs1)))
550  +ex = Equal.trans(Nat, v(x), Nat.mod(Nat.mul(v(rq), v(s1)), v(m)), Nat.mod(Nat.mul(nq, ns1), 1n+mp), e1, Equal.trans(Nat, Nat.mod(Nat.mul(v(rq), v(s1)), v(m)), Nat.mod(Nat.mul(Nat.mod(nq, 1n+mp), ns1), 1n+mp), Nat.mod(Nat.mul(nq, ns1), 1n+mp), e2, NR.mod_mul_l(mp, nq, ns1)))
551  subv(k, hk, m, mp, hm, s0, x, ns0, Nat.mod(Nat.mul(nq, ns1), 1n+mp), hs0, ex, hb0, NR.dm_lt(mp, Nat.mul(nq, ns1)), I.u32_is(NM.Lt{s0, x}), {==})
552
553def pv(p: U32 & U32) -> M.Bezout:
554  (+g, +s) = p
555  M.BZ{v(g), v(s)}
556
557def bzeq(+a: Nat, +b: Nat, +na: Nat, +nb: Nat, +ha: {a == na : Nat}, +hb: {b == nb : Nat}) -> {M.BZ{a, b} == M.BZ{na, nb} : M.Bezout}:
558  Equal.trans(M.Bezout, M.BZ{a, b}, M.BZ{na, b}, M.BZ{na, nb}, Equal.cong(Nat, M.Bezout, t => M.BZ{t, b}, a, na, ha), Equal.cong(Nat, M.Bezout, t => M.BZ{na, t}, b, nb, hb))
559
560def or_true(+x: Bool) -> {Bool.or(x, True{}) == True{} : Bool}:
561  match x:
562    case True{}:
563      {==}
564    case False{}:
565      {==}
566
567def invsim(+f: Nat, +k: Nat, +hk: {k == 32n : Nat}, +m: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}, +r0: U32, +s0: U32, +s1: U32, +r1: U32, +nr0: Nat, +ns0: Nat, +ns1: Nat, +hr0: {v(r0) == nr0 : Nat}, +hs0: {v(s0) == ns0 : Nat}, +hs1: {v(s1) == ns1 : Nat}, +hb0: {Nat.is_lt(ns0, 1n+mp) == True{} : Bool}, +cz: Bool, +nr1: Nat, +hcz: {I.u32_is(NM.IsZero{r1}) == cz : Bool}, +hr1: {v(r1) == nr1 : Nat}, +hb1: {Bool.or(Nat.is_eq(nr1, 0n), Nat.is_lt(ns1, 1n+mp)) == True{} : Bool}) -> {pv(G.inv_go(~U32, ~I.u32_op, ~I.u32_is, f, m, r0, s0, s1, (r1, cz))) == M.inv_go(f, 1n+mp, nr0, ns0, nr1, ns1) : M.Bezout}:
568  match f cz nr1:
569    case 0n _ _:
570      bzeq(v(r0), v(s0), nr0, ns0, hr0, hs0)
571    case 1n+g True{} 0n:
572      bzeq(v(r0), v(s0), nr0, ns0, hr0, hs0)
573    case 1n+g True{} 1n+rp:
574      Empty.absurd({pv(G.inv_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, m, r0, s0, s1, (r1, True{}))) == M.inv_go(1n+g, 1n+mp, nr0, ns0, 1n+rp, ns1) : M.Bezout}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{r1}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{r1}), True{}, hcz), iz(r1, 1n+rp, hr1))))
575    case 1n+g False{} 0n:
576      Empty.absurd({pv(G.inv_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, m, r0, s0, s1, (r1, False{}))) == M.inv_go(1n+g, 1n+mp, nr0, ns0, 0n, ns1) : M.Bezout}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{r1}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{r1}), True{}, iz(r1, 0n, hr1)), hcz)))
577    case 1n+ +g False{} 1n+ +rp:
578      +hnz = Equal.trans(Bool, Nat.is_eq(v(r1), 0n), Nat.is_eq(1n+rp, 0n), False{}, Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(r1), 1n+rp, hr1), {==})
579      +q = I.u32_op(NM.Quot{r0, r1})
580      +eq = Equal.trans(Nat, v(q), Nat.div(v(r0), v(r1)), Nat.div(nr0, 1n+rp), LW.ops_quot(r0, r1, hnz), Equal.trans(Nat, Nat.div(v(r0), v(r1)), Nat.div(nr0, v(r1)), Nat.div(nr0, 1n+rp), Equal.cong(Nat, Nat, t => Nat.div(t, v(r1)), v(r0), nr0, hr0), Equal.cong(Nat, Nat, t => Nat.div(nr0, t), v(r1), 1n+rp, hr1)))
581      +r2 = I.u32_op(NM.Rem{r0, r1})
582      +er2 = Equal.trans(Nat, v(r2), Nat.mod(v(r0), v(r1)), Nat.mod(nr0, 1n+rp), LW.ops_rem(r0, r1, hnz), Equal.trans(Nat, Nat.mod(v(r0), v(r1)), Nat.mod(nr0, v(r1)), Nat.mod(nr0, 1n+rp), Equal.cong(Nat, Nat, t => Nat.mod(t, v(r1)), v(r0), nr0, hr0), Equal.cong(Nat, Nat, t => Nat.mod(nr0, t), v(r1), 1n+rp, hr1)))
583      +ns2 = M.inv_step(1n+mp, Nat.div(nr0, 1n+rp), ns0, ns1)
584      +es2 = stepv(k, hk, m, mp, hm, q, s0, s1, Nat.div(nr0, 1n+rp), ns0, ns1, eq, hs0, hs1, hb0, hb1)
585      +hb2 = L.subst(Bool, t => {Bool.or(Nat.is_eq(Nat.mod(nr0, 1n+rp), 0n), t) == True{} : Bool}, True{}, Nat.is_lt(ns2, 1n+mp), Equal.sym(Bool, Nat.is_lt(ns2, 1n+mp), True{}, NR.dm_lt(mp, Nat.add(ns0, Nat.sub(1n+mp, Nat.mod(Nat.mul(Nat.div(nr0, 1n+rp), ns1), 1n+mp))))), or_true(Nat.is_eq(Nat.mod(nr0, 1n+rp), 0n)))
586      invsim(g, k, hk, m, mp, hm, r1, s1, G.inv_step(~U32, ~I.u32_op, ~I.u32_is, m, q, s0, s1), r2, 1n+rp, ns1, ns2, hr1, hs1, es2, hb1, I.u32_is(NM.IsZero{r2}), Nat.mod(nr0, 1n+rp), {==}, er2, hb2)
587
588def fin2(+m: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}, +s: U32, +sn: Nat, +hs: {v(s) == sn : Nat}, +cb: Bool, +gn: Nat, +hcb: {Bool.and(Bool.not(Nat.is_lt(gn, 1n)), Bool.not(Nat.is_lt(1n, gn))) == cb : Bool}) -> {G.inv_one(~U32, ~I.u32_op, m, s, cb) == SG.lift(~U32, ~SG.u32_of, M.inv_fin(1n+mp, M.BZ{gn, sn})) : Result<&2, &2, NM.NumError, U32>}:
589  match cb gn:
590    case True{} 1n:
591      Equal.cong(U32, Result<&2, &2, NM.NumError, U32>, t => Done{t}, I.u32_op(NM.Rem{s, m}), of(Nat.mod(sn, 1n+mp)), as_of(I.u32_op(NM.Rem{s, m}), Nat.mod(sn, 1n+mp), Equal.trans(Nat, v(I.u32_op(NM.Rem{s, m})), Nat.mod(v(s), 1n+mp), Nat.mod(sn, 1n+mp), pm_rem(s, m, mp, hm), Equal.cong(Nat, Nat, t => Nat.mod(t, 1n+mp), v(s), sn, hs))))
592    case False{} 1n:
593      Empty.absurd({G.inv_one(~U32, ~I.u32_op, m, s, False{}) == SG.lift(~U32, ~SG.u32_of, M.inv_fin(1n+mp, M.BZ{1n, sn})) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(hcb))
594    case True{} 0n:
595      Empty.absurd({G.inv_one(~U32, ~I.u32_op, m, s, True{}) == SG.lift(~U32, ~SG.u32_of, M.inv_fin(1n+mp, M.BZ{0n, sn})) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(Equal.sym(Bool, False{}, True{}, hcb)))
596    case False{} 0n:
597      {==}
598    case True{} 2n+h:
599      Empty.absurd({G.inv_one(~U32, ~I.u32_op, m, s, True{}) == SG.lift(~U32, ~SG.u32_of, M.inv_fin(1n+mp, M.BZ{2n+h, sn})) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(Equal.sym(Bool, False{}, True{}, hcb)))
600    case False{} 2n+h:
601      {==}
602
603def finsim(+m: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}, p: U32 & U32, +bz: M.Bezout, +h: {pv(p) == bz : M.Bezout}) -> {G.inv_fin(~U32, ~I.u32_op, ~I.u32_is, m, p) == SG.lift(~U32, ~SG.u32_of, M.inv_fin(1n+mp, bz)) : Result<&2, &2, NM.NumError, U32>}:
604  match p bz:
605    case Tuple{+g, +s} M.BZ{+gn, +sn}:
606      +hg = Equal.cong(M.Bezout, Nat, z => IV.bg(z), M.BZ{v(g), v(s)}, M.BZ{gn, sn}, h)
607      +hs = Equal.cong(M.Bezout, Nat, z => IV.bc(z), M.BZ{v(g), v(s)}, M.BZ{gn, sn}, h)
608      +one = I.u32_op(NM.One{})
609      +e = Equal.trans(Bool, Bool.and(Bool.not(I.u32_is(NM.Lt{g, one})), Bool.not(I.u32_is(NM.Lt{one, g}))), Bool.and(Bool.not(Nat.is_lt(gn, 1n)), Bool.not(I.u32_is(NM.Lt{one, g}))), Bool.and(Bool.not(Nat.is_lt(gn, 1n)), Bool.not(Nat.is_lt(1n, gn))), Equal.cong(Bool, Bool, t => Bool.and(Bool.not(t), Bool.not(I.u32_is(NM.Lt{one, g}))), I.u32_is(NM.Lt{g, one}), Nat.is_lt(gn, 1n), ltv(g, one, gn, 1n, hg, one_v())), Equal.cong(Bool, Bool, t => Bool.and(Bool.not(Nat.is_lt(gn, 1n)), Bool.not(t)), I.u32_is(NM.Lt{one, g}), Nat.is_lt(1n, gn), ltv(one, g, 1n, gn, one_v(), hg)))
610      fin2(m, mp, hm, s, sn, hs, Bool.and(Bool.not(I.u32_is(NM.Lt{g, one})), Bool.not(I.u32_is(NM.Lt{one, g}))), gn, Equal.sym(Bool, Bool.and(Bool.not(I.u32_is(NM.Lt{g, one})), Bool.not(I.u32_is(NM.Lt{one, g}))), Bool.and(Bool.not(Nat.is_lt(gn, 1n)), Bool.not(Nat.is_lt(1n, gn))), e))
611
612def lt1_eq(+x: Nat, +h: {Nat.is_lt(x, 1n) == True{} : Bool}) -> {Nat.is_eq(x, 0n) == True{} : Bool}:
613  match x:
614    case 0n:
615      {==}
616    case 1n+y:
617      Empty.absurd({Nat.is_eq(1n+y, 0n) == True{} : Bool}, N.lt_zero_absurd(y, h))
618
619def hb_init(+mp: Nat, +a: Nat) -> {Bool.or(Nat.is_eq(Nat.mod(a, 1n+mp), 0n), Nat.is_lt(1n, 1n+mp)) == True{} : Bool}:
620  match mp:
621    case 0n:
622      L.subst(Bool, t => {Bool.or(t, Nat.is_lt(1n, 1n)) == True{} : Bool}, True{}, Nat.is_eq(Nat.mod(a, 1n), 0n), Equal.sym(Bool, Nat.is_eq(Nat.mod(a, 1n), 0n), True{}, lt1_eq(Nat.mod(a, 1n), NR.dm_lt(0n, a))), {==})
623    case 1n+q:
624      or_true(Nat.is_eq(Nat.mod(a, 2n+q), 0n))
625
626def inv_top(+k: Nat, +hk: {k == 32n : Nat}, +a: U32, +m: U32, +c: Bool, +hc: {I.u32_is(NM.IsZero{m}) == c : Bool}, +nm: Nat, +hnm: {v(m) == nm : Nat}) -> {G.inv_ok(~U32, ~I.u32_op, ~I.u32_is, a, m, c) == SG.lift(~U32, ~SG.u32_of, M.mod_inverse(v(a), nm)) : Result<&2, &2, NM.NumError, U32>}:
627  match c nm:
628    case True{} 0n:
629      {==}
630    case False{} 0n:
631      Empty.absurd({G.inv_ok(~U32, ~I.u32_op, ~I.u32_is, a, m, False{}) == SG.lift(~U32, ~SG.u32_of, M.mod_inverse(v(a), 0n)) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{m}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{m}), True{}, iz(m, 0n, hnm)), hc)))
632    case True{} 1n+ +mp:
633      Empty.absurd({G.inv_ok(~U32, ~I.u32_op, ~I.u32_is, a, m, True{}) == SG.lift(~U32, ~SG.u32_of, M.mod_inverse(v(a), 1n+mp)) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{m}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{m}), True{}, hc), iz(m, 1n+mp, hnm))))
634    case False{} 1n+ +mp:
635      +r1 = I.u32_op(NM.Rem{a, m})
636      +ra = Nat.mod(v(a), 1n+mp)
637      +hk2 = L.subst(Nat, z => {Nat.is_le(1n+Nat.double(z), 140n) == True{} : Bool}, 32n, k, Equal.sym(Nat, k, 32n, hk), {==})
638      +s = invsim(140n, k, hk, m, mp, hnm, m, I.u32_op(NM.ZeroOp{}), I.u32_op(NM.One{}), r1, 1n+mp, 0n, 1n, hnm, zero_v(), one_v(), {==}, I.u32_is(NM.IsZero{r1}), ra, {==}, pm_rem(a, m, mp, hnm), hb_init(mp, v(a)))
639      +bz = M.inv_go(1n+mp, 1n+mp, 1n+mp, 0n, ra, 1n)
640      g = G.inv_go(~U32, ~I.u32_op, ~I.u32_is, 140n, m, m, I.u32_op(NM.ZeroOp{}), I.u32_op(NM.One{}), (r1, I.u32_is(NM.IsZero{r1})))
641      finsim(m, mp, hnm, g, bz, Equal.trans(M.Bezout, pv(g), M.inv_go(140n, 1n+mp, 1n+mp, 0n, ra, 1n), bz, s, NF.inv_140(k, mp, v(a), hk2, mv(k, hk, m, mp, hnm))))
642
643def modinv_agrees(+a: U32, +m: U32) -> SG.ModInverse.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, a, m):
644  inv_top(32n, {==}, a, m, I.u32_is(NM.IsZero{m}), {==}, v(m), {==})
645
646# ---- ilog: the multiply-up loop on the values ----
647
648def nle(+a: Nat, +b: Nat, +c: Bool, +hc: {Nat.is_lt(a, b) == c : Bool}) -> {Bool.not(c) == Nat.is_le(b, a) : Bool}:
649  match c:
650    case True{}:
651      Equal.sym(Bool, Nat.is_le(b, a), False{}, N.lt_not_le(a, b, hc))
652    case False{}:
653      Equal.sym(Bool, Nat.is_le(b, a), True{}, N.not_lt_le(a, b, hc))
654
655def nmul(+a: Nat, +b: Nat, +na: Nat, +nb: Nat, +ha: {a == na : Nat}, +hb: {b == nb : Nat}) -> {Nat.mul(a, b) == Nat.mul(na, nb) : Nat}:
656  Equal.trans(Nat, Nat.mul(a, b), Nat.mul(na, b), Nat.mul(na, nb), Equal.cong(Nat, Nat, t => Nat.mul(t, b), a, na, ha), Equal.cong(Nat, Nat, t => Nat.mul(na, t), b, nb, hb))
657
658# le(x, y) on U32 is is_le on the values
659def lev(+x: U32, +y: U32, +nx: Nat, +ny: Nat, +hx: {v(x) == nx : Nat}, +hy: {v(y) == ny : Nat}) -> {G.le(~U32, ~I.u32_is, x, y) == Nat.is_le(nx, ny) : Bool}:
660  Equal.trans(Bool, Bool.not(I.u32_is(NM.Lt{y, x})), Bool.not(Nat.is_lt(ny, nx)), Nat.is_le(nx, ny), Equal.cong(Bool, Bool, t => Bool.not(t), I.u32_is(NM.Lt{y, x}), Nat.is_lt(ny, nx), ltv(y, x, ny, nx, hy, hx)), nle(ny, nx, Nat.is_lt(ny, nx), {==}))
661
662def ilsim(+f: Nat, +q: U32, +b: U32, +k: Nat, +p: U32, +nn: Nat, +bq: Nat, +np: Nat, +hq: {v(q) == Nat.div(nn, 2n+bq) : Nat}, +hb: {v(b) == 2n+bq : Nat}, +hp: {v(p) == np : Nat}, +K: Nat, +hK: {K == 32n : Nat}, +hn: {Nat.is_lt(nn, C.pow2(K)) == True{} : Bool}, +up: Bool, +hup: {up == Nat.is_le(np, Nat.div(nn, 2n+bq)) : Bool}) -> {G.ilog_go(~U32, ~I.u32_op, ~I.u32_is, f, q, b, k, p, up) == M.ilog_go(f, nn, 2n+bq, k, np, up) : Nat}:
663  match f up:
664    case 0n _:
665      {==}
666    case 1n+g False{}:
667      {==}
668    case 1n+ +g True{}:
669      +hle = Equal.sym(Bool, True{}, Nat.is_le(np, Nat.div(nn, 2n+bq)), hup)
670      +hmn = Equal.trans(Bool, Nat.is_le(Nat.mul(np, 2n+bq), nn), Nat.is_le(np, Nat.div(nn, 2n+bq)), True{}, Equal.sym(Bool, Nat.is_le(np, Nat.div(nn, 2n+bq)), Nat.is_le(Nat.mul(np, 2n+bq), nn), NR.le_div(1n+bq, np, nn)), hle)
671      +emul = nmul(v(p), v(b), np, 2n+bq, hp, hb)
672      +hfit = fits32(K, hK, Nat.mul(v(p), v(b)), L.subst(Nat, z => {Nat.is_lt(z, C.pow2(K)) == True{} : Bool}, Nat.mul(np, 2n+bq), Nat.mul(v(p), v(b)), Equal.sym(Nat, Nat.mul(v(p), v(b)), Nat.mul(np, 2n+bq), emul), N.le_lt_trans(Nat.mul(np, 2n+bq), nn, C.pow2(K), hmn, hn)))
673      +hmo = Equal.trans(Bool, I.u32_is(NM.MulOver{p, b}), Bool.not(C.fits(32n, Nat.mul(v(p), v(b)))), False{}, LW.tests_mul_over(p, b), Equal.cong(Bool, Bool, t => Bool.not(t), C.fits(32n, Nat.mul(v(p), v(b))), True{}, hfit))
674      +pb = I.u32_op(NM.Mul{p, b})
675      +epb = Equal.trans(Nat, v(pb), Nat.mul(v(p), v(b)), Nat.mul(np, 2n+bq), LW.ops_mul(p, b, hmo), emul)
676      +u2 = G.le(~U32, ~I.u32_is, pb, q)
677      +hu2 = lev(pb, q, Nat.mul(np, 2n+bq), Nat.div(nn, 2n+bq), epb, hq)
678      Equal.trans(Nat, G.ilog_go(~U32, ~I.u32_op, ~I.u32_is, g, q, b, 1n+k, pb, u2), M.ilog_go(g, nn, 2n+bq, 1n+k, Nat.mul(np, 2n+bq), u2), M.ilog_go(g, nn, 2n+bq, 1n+k, Nat.mul(np, 2n+bq), Nat.is_le(Nat.mul(np, 2n+bq), Nat.div(nn, 2n+bq))), ilsim(g, q, b, 1n+k, pb, nn, bq, Nat.mul(np, 2n+bq), hq, hb, epb, K, hK, hn, u2, hu2), Equal.cong(Bool, Nat, t => M.ilog_go(g, nn, 2n+bq, 1n+k, Nat.mul(np, 2n+bq), t), u2, Nat.is_le(Nat.mul(np, 2n+bq), Nat.div(nn, 2n+bq)), hu2))
679
680def or_false_r(+x: Bool, +y: Bool, +h: {Bool.or(x, y) == False{} : Bool}) -> {y == False{} : Bool}:
681  match x:
682    case True{}:
683      Empty.absurd({y == False{} : Bool}, true_ne_false(h))
684    case False{}:
685      h
686
687def ilog_fin(+K: Nat, +hK: {K == 32n : Nat}, +n: U32, +b: U32, +nb: Nat, +hb: {v(b) == nb : Nat}, +hl: {Nat.is_lt(nb, 2n) == False{} : Bool}) -> {G.ilog_ok(~U32, ~I.u32_op, ~I.u32_is, n, b, False{}) == SG.lift_nat(M.ilog_ok(v(n), nb, False{})) : Result<&2, &2, NM.NumError, Nat>}:
688  match nb:
689    case 0n:
690      Empty.absurd({G.ilog_ok(~U32, ~I.u32_op, ~I.u32_is, n, b, False{}) == SG.lift_nat(M.ilog_ok(v(n), 0n, False{})) : Result<&2, &2, NM.NumError, Nat>}, true_ne_false(hl))
691    case 1n:
692      Empty.absurd({G.ilog_ok(~U32, ~I.u32_op, ~I.u32_is, n, b, False{}) == SG.lift_nat(M.ilog_ok(v(n), 1n, False{})) : Result<&2, &2, NM.NumError, Nat>}, true_ne_false(hl))
693    case 2n+ +bq:
694      +hnz = Equal.trans(Bool, Nat.is_eq(v(b), 0n), Nat.is_eq(2n+bq, 0n), False{}, Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(b), 2n+bq, hb), {==})
695      +q = I.u32_op(NM.Quot{n, b})
696      +dq = Nat.div(v(n), 2n+bq)
697      +eq = Equal.trans(Nat, v(q), Nat.div(v(n), v(b)), dq, LW.ops_quot(n, b, hnz), Equal.cong(Nat, Nat, t => Nat.div(v(n), t), v(b), 2n+bq, hb))
698      +one = I.u32_op(NM.One{})
699      +up = G.le(~U32, ~I.u32_is, one, q)
700      +hup = lev(one, q, 1n, dq, one_v(), eq)
701      +hn = U32P.val_lt(1n, {==}, K, hK, n)
702      +hK2 = L.subst(Nat, z => {Nat.is_le(z, 140n) == True{} : Bool}, 32n, K, Equal.sym(Nat, K, 32n, hK), {==})
703      +s = ilsim(140n, q, b, 0n, one, v(n), bq, 1n, eq, hb, one_v(), K, hK, hn, up, hup)
704      +c1 = Equal.cong(Bool, Nat, t => M.ilog_go(140n, v(n), 2n+bq, 0n, 1n, t), up, Nat.is_le(1n, dq), hup)
705      +c2 = NF.il_140(K, v(n), bq, hK2, N.le_lt_trans(dq, v(n), C.pow2(K), AR2.div_le(v(n), 2n+bq), hn))
706      +r = M.ilog_go(v(n), v(n), 2n+bq, 0n, 1n, Nat.is_le(1n, dq))
707      Equal.cong(Nat, Result<&2, &2, NM.NumError, Nat>, t => Done{t}, G.ilog_go(~U32, ~I.u32_op, ~I.u32_is, 140n, q, b, 0n, one, up), r, Equal.trans(Nat, G.ilog_go(~U32, ~I.u32_op, ~I.u32_is, 140n, q, b, 0n, one, up), M.ilog_go(140n, v(n), 2n+bq, 0n, 1n, up), r, s, Equal.trans(Nat, M.ilog_go(140n, v(n), 2n+bq, 0n, 1n, up), M.ilog_go(140n, v(n), 2n+bq, 0n, 1n, Nat.is_le(1n, dq)), r, c1, c2)))
708
709def ilog_top(+K: Nat, +hK: {K == 32n : Nat}, +n: U32, +b: U32, +bad: Bool, +hN: {Bool.or(Nat.is_eq(v(n), 0n), Nat.is_lt(v(b), 2n)) == bad : Bool}) -> {G.ilog_ok(~U32, ~I.u32_op, ~I.u32_is, n, b, bad) == SG.lift_nat(M.ilog_ok(v(n), v(b), bad)) : Result<&2, &2, NM.NumError, Nat>}:
710  match bad:
711    case True{}:
712      {==}
713    case False{}:
714      ilog_fin(K, hK, n, b, v(b), {==}, or_false_r(Nat.is_eq(v(n), 0n), Nat.is_lt(v(b), 2n), hN))
715
716def two_v() -> {v(I.u32_op(NM.Add{I.u32_op(NM.One{}), I.u32_op(NM.One{})})) == 2n : Nat}:
717  +one = I.u32_op(NM.One{})
718  +e11 = nadd(v(one), v(one), 1n, 1n, one_v(), one_v())
719  +hao = Equal.trans(Bool, I.u32_is(NM.AddOver{one, one}), Bool.not(C.fits(32n, Nat.add(v(one), v(one)))), False{}, LW.tests_add_over(one, one), Equal.cong(Nat, Bool, t => Bool.not(C.fits(32n, t)), Nat.add(v(one), v(one)), 2n, e11))
720  Equal.trans(Nat, v(I.u32_op(NM.Add{one, one})), Nat.add(v(one), v(one)), 2n, LW.ops_add(one, one, hao), e11)
721
722def ilog_agrees(+n: U32, +b: U32) -> SG.Ilog.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, n, b):
723  +two = I.u32_op(NM.Add{I.u32_op(NM.One{}), I.u32_op(NM.One{})})
724  +bu = Bool.or(I.u32_is(NM.IsZero{n}), I.u32_is(NM.Lt{b, two}))
725  +bn = Bool.or(Nat.is_eq(v(n), 0n), Nat.is_lt(v(b), 2n))
726  +eb = Equal.trans(Bool, bu, Bool.or(Nat.is_eq(v(n), 0n), I.u32_is(NM.Lt{b, two})), bn, Equal.cong(Bool, Bool, t => Bool.or(t, I.u32_is(NM.Lt{b, two})), I.u32_is(NM.IsZero{n}), Nat.is_eq(v(n), 0n), LW.tests_is_zero(n)), Equal.cong(Bool, Bool, t => Bool.or(Nat.is_eq(v(n), 0n), t), I.u32_is(NM.Lt{b, two}), Nat.is_lt(v(b), 2n), ltv(b, two, v(b), 2n, {==}, two_v())))
727  Equal.trans(Result<&2, &2, NM.NumError, Nat>, G.ilog_ok(~U32, ~I.u32_op, ~I.u32_is, n, b, bu), SG.lift_nat(M.ilog_ok(v(n), v(b), bu)), SG.lift_nat(M.ilog_ok(v(n), v(b), bn)), ilog_top(32n, {==}, n, b, bu, Equal.sym(Bool, bu, bn, eb)), Equal.cong(Bool, Result<&2, &2, NM.NumError, Nat>, t => SG.lift_nat(M.ilog_ok(v(n), v(b), t)), bu, bn, eb))
728
729# ---- factorial: 2 * 3 * ... bottom-up, stopping at the first overflow ----
730
731# the value when the flag says it fits
732def FR(ok: Bool, a: U32, x: Nat) -> Type:
733  match ok:
734    case True{}:
735      {v(a) == x : Nat}
736    case False{}:
737      {x == x : Nat}
738
739def not_not(+c: Bool) -> {Bool.not(Bool.not(c)) == c : Bool}:
740  match c:
741    case True{}:
742      {==}
743    case False{}:
744      {==}
745
746def fr_mul(+a: U32, +x: U32, +n: Nat, +hn: {Nat.mul(v(a), v(x)) == n : Nat}, +c: Bool, +hc: {C.fits(32n, n) == c : Bool}) -> FR(Bool.not(I.u32_is(NM.MulOver{a, x})), I.u32_op(NM.Mul{a, x}), n):
747  match c:
748    case True{}:
749      +hmo = mo_of(a, x, n, hn, True{}, hc)
750      %Equal.sym(Bool, I.u32_is(NM.MulOver{a, x}), False{}, hmo) : FR(Bool.not(_), I.u32_op(NM.Mul{a, x}), n)
751      Equal.trans(Nat, v(I.u32_op(NM.Mul{a, x})), Nat.mul(v(a), v(x)), n, LW.ops_mul(a, x, hmo), hn)
752    case False{}:
753      %Equal.sym(Bool, I.u32_is(NM.MulOver{a, x}), True{}, mo_of(a, x, n, hn, False{}, hc)) : FR(Bool.not(_), I.u32_op(NM.Mul{a, x}), n)
754      {==}
755
756# the flag after a checked multiply is fits(product)
757def ok_mul(+a: U32, +x: U32, +n: Nat, +hn: {Nat.mul(v(a), v(x)) == n : Nat}) -> {C.fits(32n, n) == Bool.not(I.u32_is(NM.MulOver{a, x})) : Bool}:
758  Equal.sym(Bool, Bool.not(I.u32_is(NM.MulOver{a, x})), C.fits(32n, n), Equal.trans(Bool, Bool.not(I.u32_is(NM.MulOver{a, x})), Bool.not(Bool.not(C.fits(32n, n))), C.fits(32n, n), Equal.cong(Bool, Bool, t => Bool.not(t), I.u32_is(NM.MulOver{a, x}), Bool.not(C.fits(32n, n)), mo_of(a, x, n, hn, C.fits(32n, n), {==})), not_not(C.fits(32n, n))))
759
760def fk(+K: Nat, +hK: {K == 32n : Nat}, +x: Nat, +h: {C.fits(32n, x) == True{} : Bool}) -> {Nat.is_lt(x, C.pow2(K)) == True{} : Bool}:
761  +h2 = L.subst(Nat, z => {C.fits(z, x) == True{} : Bool}, 32n, K, Equal.sym(Nat, K, 32n, hK), h)
762  Equal.trans(Bool, Nat.is_lt(x, C.pow2(K)), C.fits(K, x), True{}, Equal.sym(Bool, C.fits(K, x), Nat.is_lt(x, C.pow2(K)), WW.fits_lt(K, x)), h2)
763
764def succ_le(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_le(1n+a, b) == True{} : Bool}:
765  match a b:
766    case _ 0n:
767      Empty.absurd({Nat.is_le(1n+a, 0n) == True{} : Bool}, N.lt_zero_absurd(a, h))
768    case 0n 1n+y:
769      N.zero_le(y)
770    case 1n+ +x 1n+ +y:
771      succ_le(x, y, h)
772
773def plus1(+x: Nat) -> {Nat.add(x, 1n) == 1n+x : Nat}:
774  Equal.trans(Nat, Nat.add(x, 1n), 1n+Nat.add(x, 0n), 1n+x, NA.add_succ(x, 0n), Equal.cong(Nat, Nat, t => 1n+t, Nat.add(x, 0n), x, N.add_zero(x)))
775
776# inc(i) for i < n is i + 1
777def inc_v(+K: Nat, +hK: {K == 32n : Nat}, +i: U32, +n: U32, +ni: Nat, +nn: Nat, +hi: {v(i) == ni : Nat}, +hn: {v(n) == nn : Nat}, +hlt: {Nat.is_lt(ni, nn) == True{} : Bool}) -> {v(G.inc(~U32, ~I.u32_op, i)) == 1n+ni : Nat}:
778  +one = I.u32_op(NM.One{})
779  +hnK = L.subst(Nat, z => {Nat.is_lt(z, C.pow2(K)) == True{} : Bool}, v(n), nn, hn, U32P.val_lt(1n, {==}, K, hK, n))
780  +hfit = fits32(K, hK, 1n+ni, N.le_lt_trans(1n+ni, nn, C.pow2(K), succ_le(ni, nn, hlt), hnK))
781  +hn1 = Equal.trans(Nat, Nat.add(v(i), v(one)), Nat.add(ni, 1n), 1n+ni, nadd(v(i), v(one), ni, 1n, hi, one_v()), plus1(ni))
782  Equal.trans(Nat, v(I.u32_op(NM.Add{i, one})), Nat.add(v(i), v(one)), 1n+ni, LW.ops_add(i, one, ao_of(i, one, 1n+ni, hn1, True{}, hfit)), hn1)
783
784def factsim(+f: Nat, +i: U32, +n: U32, +a: U32, +ni: Nat, +nn: Nat, +K: Nat, +ok: Bool, +more: Bool, +cn: Bool, +hK: {K == 32n : Nat}, +hi: {v(i) == ni : Nat}, +hn: {v(n) == nn : Nat}, +hmono: {Nat.is_le(S.factorial(ni), S.factorial(nn)) == True{} : Bool}, +hf: {Nat.is_le(1n+K, Nat.add(f, ni)) == True{} : Bool}, +hok: {C.fits(32n, S.factorial(ni)) == ok : Bool}, ha: FR(ok, a, S.factorial(ni)), +hmore: {more == Nat.is_lt(ni, nn) : Bool}, +hcn: {C.fits(32n, S.factorial(nn)) == cn : Bool}) -> {G.fact_go(~U32, ~I.u32_op, ~I.u32_is, f, i, n, (a, ok), more) == G.fits(U32, Bool.not(cn), of(S.factorial(nn))) : Maybe<&2, U32>}:
785  match f ok more cn:
786    case 0n True{} _ _:
787      +big = NF.fbig(K, ni, hf)
788      Empty.absurd({G.fact_go(~U32, ~I.u32_op, ~I.u32_is, 0n, i, n, (a, True{}), more) == G.fits(U32, Bool.not(cn), of(S.factorial(nn))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(S.factorial(ni), C.pow2(K)), False{}, Equal.sym(Bool, Nat.is_lt(S.factorial(ni), C.pow2(K)), True{}, fk(K, hK, S.factorial(ni), hok)), N.le_not_lt(S.factorial(ni), C.pow2(K), big))))
789    case 0n False{} _ True{}:
790      Empty.absurd({G.fact_go(~U32, ~I.u32_op, ~I.u32_is, 0n, i, n, (a, False{}), more) == G.fits(U32, Bool.not(True{}), of(S.factorial(nn))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, S.factorial(nn)), False{}, Equal.sym(Bool, C.fits(32n, S.factorial(nn)), True{}, hcn), unfit_mono(32n, S.factorial(ni), S.factorial(nn), hmono, hok))))
791    case 0n False{} _ False{}:
792      {==}
793    case 1n+g False{} _ True{}:
794      Empty.absurd({G.fact_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, i, n, (a, False{}), more) == G.fits(U32, Bool.not(True{}), of(S.factorial(nn))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, S.factorial(nn)), False{}, Equal.sym(Bool, C.fits(32n, S.factorial(nn)), True{}, hcn), unfit_mono(32n, S.factorial(ni), S.factorial(nn), hmono, hok))))
795    case 1n+g False{} _ False{}:
796      {==}
797    case 1n+g True{} False{} True{}:
798      +eqF = N.le_antisym(S.factorial(ni), S.factorial(nn), hmono, NF.fmono(nn, ni, N.not_lt_le(ni, nn, Equal.sym(Bool, False{}, Nat.is_lt(ni, nn), hmore))))
799      Equal.cong(U32, Maybe<&2, U32>, t => Some{t}, a, of(S.factorial(nn)), as_of(a, S.factorial(nn), Equal.trans(Nat, v(a), S.factorial(ni), S.factorial(nn), ha, eqF)))
800    case 1n+g True{} False{} False{}:
801      +eqF = N.le_antisym(S.factorial(ni), S.factorial(nn), hmono, NF.fmono(nn, ni, N.not_lt_le(ni, nn, Equal.sym(Bool, False{}, Nat.is_lt(ni, nn), hmore))))
802      Empty.absurd({G.fact_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, i, n, (a, True{}), False{}) == G.fits(U32, Bool.not(False{}), of(S.factorial(nn))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, S.factorial(ni)), False{}, Equal.sym(Bool, C.fits(32n, S.factorial(ni)), True{}, hok), Equal.trans(Bool, C.fits(32n, S.factorial(ni)), C.fits(32n, S.factorial(nn)), False{}, Equal.cong(Nat, Bool, t => C.fits(32n, t), S.factorial(ni), S.factorial(nn), eqF), hcn))))
803    case 1n+ +g True{} True{} _:
804      +hlt = Equal.sym(Bool, True{}, Nat.is_lt(ni, nn), hmore)
805      +x = G.inc(~U32, ~I.u32_op, i)
806      +ex = inc_v(K, hK, i, n, ni, nn, hi, hn, hlt)
807      +pn = S.factorial(1n+ni)
808      +hpn = Equal.trans(Nat, Nat.mul(v(a), v(x)), Nat.mul(S.factorial(ni), 1n+ni), pn, nmul(v(a), v(x), S.factorial(ni), 1n+ni, ha, ex), NA.mul_comm(S.factorial(ni), 1n+ni))
809      +hf2 = L.subst(Nat, z => {Nat.is_le(1n+K, z) == True{} : Bool}, 1n+Nat.add(g, ni), Nat.add(g, 1n+ni), Equal.sym(Nat, Nat.add(g, 1n+ni), 1n+Nat.add(g, ni), NA.add_succ(g, ni)), hf)
810      factsim(g, x, n, I.u32_op(NM.Mul{a, x}), 1n+ni, nn, K, Bool.not(I.u32_is(NM.MulOver{a, x})), I.u32_is(NM.Lt{x, n}), cn, hK, ex, hn, NF.fmono(1n+ni, nn, succ_le(ni, nn, hlt)), hf2, ok_mul(a, x, pn, hpn), fr_mul(a, x, pn, hpn, C.fits(32n, pn), {==}), ltv(x, n, 1n+ni, nn, ex, hn), hcn)
811
812def okfits(+x: Nat, +c: Bool) -> {G.ok(U32, G.fits(U32, Bool.not(c), of(x))) == SG.checked_pick(~U32, ~SG.u32_of, x, c) : Result<&2, &2, NM.NumError, U32>}:
813  match c:
814    case True{}:
815      {==}
816    case False{}:
817      {==}
818
819def fact_top(+K: Nat, +hK: {K == 32n : Nat}, +n: U32) -> SG.Factorial.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, n):
820  +one = I.u32_op(NM.One{})
821  +F = S.factorial(v(n))
822  +hf0 = L.subst(Nat, z => {Nat.is_le(1n+z, 141n) == True{} : Bool}, 32n, K, Equal.sym(Nat, K, 32n, hK), {==})
823  +s = factsim(140n, one, n, one, 1n, v(n), K, True{}, I.u32_is(NM.Lt{one, n}), C.fits(32n, F), hK, one_v(), {==}, NF.fmono(0n, v(n), N.zero_le(v(n))), hf0, {==}, one_v(), ltv(one, n, 1n, v(n), one_v(), {==}), {==})
824  +g = G.fact_go(~U32, ~I.u32_op, ~I.u32_is, 140n, one, n, (one, True{}), I.u32_is(NM.Lt{one, n}))
825  Equal.trans(Result<&2, &2, NM.NumError, U32>, G.ok(U32, g), SG.checked_pick(~U32, ~SG.u32_of, F, C.fits(32n, F)), SG.checked(~U32, ~SG.u32_of, 32n, M.factorial(v(n))), Equal.trans(Result<&2, &2, NM.NumError, U32>, G.ok(U32, g), G.ok(U32, G.fits(U32, Bool.not(C.fits(32n, F)), of(F))), SG.checked_pick(~U32, ~SG.u32_of, F, C.fits(32n, F)), Equal.cong(Maybe<&2, U32>, Result<&2, &2, NM.NumError, U32>, t => G.ok(U32, t), g, G.fits(U32, Bool.not(C.fits(32n, F)), of(F)), s), okfits(F, C.fits(32n, F))), Equal.cong(Nat, Result<&2, &2, NM.NumError, U32>, t => SG.checked(~U32, ~SG.u32_of, 32n, t), F, M.factorial(v(n)), Equal.sym(Nat, M.factorial(v(n)), F, FA.factorial_ok(v(n)))))
826
827def factorial_checked(+n: U32) -> SG.Factorial.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, n):
828  fact_top(32n, {==}, n)
829
830# ---- perm: n (n - 1) ... multiplied top-down, j factors taken, r left ----
831
832def pmon(+nn: Nat, +j: Nat, +r: Nat, +k0: Nat, +hj: {Nat.add(j, r) == k0 : Nat}, +hle: {Nat.is_le(k0, nn) == True{} : Bool}) -> {Nat.is_le(S.desc(nn, j), S.desc(nn, k0)) == True{} : Bool}:
833  +h1 = NF.dmono(nn, j, r, L.subst(Nat, z => {Nat.is_le(z, nn) == True{} : Bool}, k0, Nat.add(j, r), Equal.sym(Nat, Nat.add(j, r), k0, hj), hle))
834  L.subst(Nat, z => {Nat.is_le(S.desc(nn, j), S.desc(nn, z)) == True{} : Bool}, Nat.add(j, r), k0, hj, h1)
835
836def le_v(+a: U32, +b: U32, +na: Nat, +nb: Nat, +ha: {v(a) == na : Nat}, +hb: {v(b) == nb : Nat}, +h: {Nat.is_le(na, nb) == True{} : Bool}) -> {Nat.is_le(v(a), v(b)) == True{} : Bool}:
837  +h1 = L.subst(Nat, z => {Nat.is_le(z, nb) == True{} : Bool}, na, v(a), Equal.sym(Nat, v(a), na, ha), h)
838  L.subst(Nat, z => {Nat.is_le(v(a), z) == True{} : Bool}, nb, v(b), Equal.sym(Nat, v(b), nb, hb), h1)
839
840def permsim(+f: Nat, +k: U32, +m: U32, +a: U32, +nn: Nat, +j: Nat, +r: Nat, +k0: Nat, +K: Nat, +ok: Bool, +more: Bool, +cn: Bool, +hK: {K == 32n : Nat}, +hkr: {v(k) == r : Nat}, +hm: {v(m) == Nat.sub(nn, j) : Nat}, +hj: {Nat.add(j, r) == k0 : Nat}, +hle: {Nat.is_le(k0, nn) == True{} : Bool}, +hf: {Nat.is_le(1n+K, Nat.add(f, j)) == True{} : Bool}, +hok: {C.fits(32n, S.desc(nn, j)) == ok : Bool}, ha: FR(ok, a, S.desc(nn, j)), +hmore: {more == Bool.not(Nat.is_eq(r, 0n)) : Bool}, +hcn: {C.fits(32n, S.desc(nn, k0)) == cn : Bool}) -> {G.perm_go(~U32, ~I.u32_op, ~I.u32_is, f, k, m, (a, ok), more) == G.fits(U32, Bool.not(cn), of(S.desc(nn, k0))) : Maybe<&2, U32>}:
841  match f r ok more cn:
842    case 0n _ True{} _ _:
843      +hjk = L.subst(Nat, z => {Nat.is_le(j, z) == True{} : Bool}, Nat.add(j, r), k0, hj, N.le_add_right(j, r))
844      +big = NF.dbig(K, nn, j, hf, N.le_trans(j, k0, nn, hjk, hle))
845      Empty.absurd({G.perm_go(~U32, ~I.u32_op, ~I.u32_is, 0n, k, m, (a, True{}), more) == G.fits(U32, Bool.not(cn), of(S.desc(nn, k0))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(S.desc(nn, j), C.pow2(K)), False{}, Equal.sym(Bool, Nat.is_lt(S.desc(nn, j), C.pow2(K)), True{}, fk(K, hK, S.desc(nn, j), hok)), N.le_not_lt(S.desc(nn, j), C.pow2(K), big))))
846    case 0n _ False{} _ True{}:
847      Empty.absurd({G.perm_go(~U32, ~I.u32_op, ~I.u32_is, 0n, k, m, (a, False{}), more) == G.fits(U32, Bool.not(True{}), of(S.desc(nn, k0))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, S.desc(nn, k0)), False{}, Equal.sym(Bool, C.fits(32n, S.desc(nn, k0)), True{}, hcn), unfit_mono(32n, S.desc(nn, j), S.desc(nn, k0), pmon(nn, j, r, k0, hj, hle), hok))))
848    case 0n _ False{} _ False{}:
849      {==}
850    case 1n+g _ False{} _ True{}:
851      Empty.absurd({G.perm_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, k, m, (a, False{}), more) == G.fits(U32, Bool.not(True{}), of(S.desc(nn, k0))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, S.desc(nn, k0)), False{}, Equal.sym(Bool, C.fits(32n, S.desc(nn, k0)), True{}, hcn), unfit_mono(32n, S.desc(nn, j), S.desc(nn, k0), pmon(nn, j, r, k0, hj, hle), hok))))
852    case 1n+g _ False{} _ False{}:
853      {==}
854    case 1n+g 0n True{} False{} True{}:
855      +ejk = Equal.trans(Nat, j, Nat.add(j, 0n), k0, Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j)), hj)
856      Equal.cong(U32, Maybe<&2, U32>, t => Some{t}, a, of(S.desc(nn, k0)), as_of(a, S.desc(nn, k0), Equal.trans(Nat, v(a), S.desc(nn, j), S.desc(nn, k0), ha, Equal.cong(Nat, Nat, t => S.desc(nn, t), j, k0, ejk))))
857    case 1n+g 0n True{} False{} False{}:
858      +ejk = Equal.trans(Nat, j, Nat.add(j, 0n), k0, Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j)), hj)
859      Empty.absurd({G.perm_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, k, m, (a, True{}), False{}) == G.fits(U32, Bool.not(False{}), of(S.desc(nn, k0))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, S.desc(nn, j)), False{}, Equal.sym(Bool, C.fits(32n, S.desc(nn, j)), True{}, hok), Equal.trans(Bool, C.fits(32n, S.desc(nn, j)), C.fits(32n, S.desc(nn, k0)), False{}, Equal.cong(Nat, Bool, t => C.fits(32n, S.desc(nn, t)), j, k0, ejk), hcn))))
860    case 1n+g 1n+rp True{} False{} _:
861      Empty.absurd({G.perm_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, k, m, (a, True{}), False{}) == G.fits(U32, Bool.not(cn), of(S.desc(nn, k0))) : Maybe<&2, U32>}, true_ne_false(Equal.sym(Bool, False{}, True{}, hmore)))
862    case 1n+g 0n True{} True{} _:
863      Empty.absurd({G.perm_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, k, m, (a, True{}), True{}) == G.fits(U32, Bool.not(cn), of(S.desc(nn, k0))) : Maybe<&2, U32>}, true_ne_false(hmore))
864    case 1n+ +g 1n+ +rp True{} True{} _:
865      +one = I.u32_op(NM.One{})
866      +es = NA.add_succ(j, rp)
867      +hj1 = N.le_lt_trans(j, Nat.add(j, rp), 1n+Nat.add(j, rp), N.le_add_right(j, rp), N.lt_succ(Nat.add(j, rp)))
868      +hj2 = L.subst(Nat, z => {Nat.is_lt(j, z) == True{} : Bool}, 1n+Nat.add(j, rp), k0, Equal.trans(Nat, 1n+Nat.add(j, rp), Nat.add(j, 1n+rp), k0, Equal.sym(Nat, Nat.add(j, 1n+rp), 1n+Nat.add(j, rp), es), hj), hj1)
869      +hjn = N.lt_le_trans(j, k0, nn, hj2, hle)
870      +X = Nat.sub(nn, 1n+j)
871      +esx = FA.sub_lt_succ(nn, j, hjn)
872      +hpn = Equal.trans(Nat, Nat.mul(v(a), v(m)), Nat.mul(S.desc(nn, j), Nat.sub(nn, j)), S.desc(nn, 1n+j), nmul(v(a), v(m), S.desc(nn, j), Nat.sub(nn, j), ha, hm), NA.mul_comm(S.desc(nn, j), Nat.sub(nn, j)))
873      +dk = G.dec(~U32, ~I.u32_op, k)
874      +edk = Equal.trans(Nat, v(dk), Nat.sub(v(k), v(one)), rp, LW.ops_sub(k, one, le_v(one, k, 1n, 1n+rp, one_v(), hkr, N.zero_le(rp))), Equal.trans(Nat, Nat.sub(v(k), v(one)), Nat.sub(1n+rp, 1n), rp, nsub(v(k), v(one), 1n+rp, 1n, hkr, one_v()), N.sub_zero(rp)))
875      +emx = Equal.trans(Nat, v(m), Nat.sub(nn, j), 1n+X, hm, esx)
876      +dm2 = G.dec(~U32, ~I.u32_op, m)
877      +edm = Equal.trans(Nat, v(dm2), Nat.sub(v(m), v(one)), X, LW.ops_sub(m, one, le_v(one, m, 1n, 1n+X, one_v(), emx, N.zero_le(X))), Equal.trans(Nat, Nat.sub(v(m), v(one)), Nat.sub(1n+X, 1n), X, nsub(v(m), v(one), 1n+X, 1n, emx, one_v()), N.sub_zero(X)))
878      +hmore2 = Equal.cong(Bool, Bool, t => Bool.not(t), I.u32_is(NM.IsZero{dk}), Nat.is_eq(rp, 0n), iz(dk, rp, edk))
879      +hjj = Equal.trans(Nat, 1n+Nat.add(j, rp), Nat.add(j, 1n+rp), k0, Equal.sym(Nat, Nat.add(j, 1n+rp), 1n+Nat.add(j, rp), es), hj)
880      +hf2 = L.subst(Nat, z => {Nat.is_le(1n+K, z) == True{} : Bool}, 1n+Nat.add(g, j), Nat.add(g, 1n+j), Equal.sym(Nat, Nat.add(g, 1n+j), 1n+Nat.add(g, j), NA.add_succ(g, j)), hf)
881      +pn = S.desc(nn, 1n+j)
882      permsim(g, dk, dm2, I.u32_op(NM.Mul{a, m}), nn, 1n+j, rp, k0, K, Bool.not(I.u32_is(NM.MulOver{a, m})), Bool.not(I.u32_is(NM.IsZero{dk})), cn, hK, edk, edm, hjj, hle, hf2, ok_mul(a, m, pn, hpn), fr_mul(a, m, pn, hpn, C.fits(32n, pn), {==}), hmore2, hcn)
883
884def perm_top(+K: Nat, +hK: {K == 32n : Nat}, +n: U32, +k: U32, +big: Bool, +hbig: {I.u32_is(NM.Lt{n, k}) == big : Bool}) -> {G.perm_big(~U32, ~I.u32_op, ~I.u32_is, n, k, big) == SG.checked(~U32, ~SG.u32_of, 32n, S.desc(v(n), v(k))) : Result<&2, &2, NM.NumError, U32>}:
885  match big:
886    case True{}:
887      +dz = NF.desc_zero(v(n), v(k), lt_of(n, k, True{}, hbig))
888      Equal.trans(Result<&2, &2, NM.NumError, U32>, Done{I.u32_op(NM.ZeroOp{})}, SG.checked(~U32, ~SG.u32_of, 32n, 0n), SG.checked(~U32, ~SG.u32_of, 32n, S.desc(v(n), v(k))), Equal.cong(U32, Result<&2, &2, NM.NumError, U32>, t => Done{t}, I.u32_op(NM.ZeroOp{}), of(0n), as_of(I.u32_op(NM.ZeroOp{}), 0n, zero_v())), Equal.cong(Nat, Result<&2, &2, NM.NumError, U32>, t => SG.checked(~U32, ~SG.u32_of, 32n, t), 0n, S.desc(v(n), v(k)), Equal.sym(Nat, S.desc(v(n), v(k)), 0n, dz)))
889    case False{}:
890      +one = I.u32_op(NM.One{})
891      +D = S.desc(v(n), v(k))
892      +hge = N.not_lt_le(v(n), v(k), lt_of(n, k, False{}, hbig))
893      +hf0 = L.subst(Nat, z => {Nat.is_le(1n+z, 140n) == True{} : Bool}, 32n, K, Equal.sym(Nat, K, 32n, hK), {==})
894      +hm0 = Equal.sym(Nat, Nat.sub(v(n), 0n), v(n), N.sub_zero(v(n)))
895      +more = Bool.not(I.u32_is(NM.IsZero{k}))
896      +hmore = Equal.cong(Bool, Bool, t => Bool.not(t), I.u32_is(NM.IsZero{k}), Nat.is_eq(v(k), 0n), iz(k, v(k), {==}))
897      +s = permsim(140n, k, n, one, v(n), 0n, v(k), v(k), K, True{}, more, C.fits(32n, D), hK, {==}, hm0, {==}, hge, hf0, {==}, one_v(), hmore, {==})
898      +g = G.perm_go(~U32, ~I.u32_op, ~I.u32_is, 140n, k, n, (one, True{}), more)
899      Equal.trans(Result<&2, &2, NM.NumError, U32>, G.ok(U32, g), G.ok(U32, G.fits(U32, Bool.not(C.fits(32n, D)), of(D))), SG.checked(~U32, ~SG.u32_of, 32n, D), Equal.cong(Maybe<&2, U32>, Result<&2, &2, NM.NumError, U32>, t => G.ok(U32, t), g, G.fits(U32, Bool.not(C.fits(32n, D)), of(D)), s), okfits(D, C.fits(32n, D)))
900
901def perm_checked(+n: U32, +k: U32) -> SG.Perm.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, n, k):
902  Equal.trans(Result<&2, &2, NM.NumError, U32>, G.perm_big(~U32, ~I.u32_op, ~I.u32_is, n, k, I.u32_is(NM.Lt{n, k})), SG.checked(~U32, ~SG.u32_of, 32n, S.desc(v(n), v(k))), SG.checked(~U32, ~SG.u32_of, 32n, M.perm(v(n), v(k))), perm_top(32n, {==}, n, k, I.u32_is(NM.Lt{n, k}), {==}), Equal.cong(Nat, Result<&2, &2, NM.NumError, U32>, t => SG.checked(~U32, ~SG.u32_of, 32n, t), S.desc(v(n), v(k)), M.perm(v(n), v(k)), Equal.sym(Nat, M.perm(v(n), v(k)), S.desc(v(n), v(k)), FA.perm_ok(v(n), v(k)))))
903
904# ---- pow: square-and-multiply with fit flags ----
905
906# y when ok, else x: {fv(ok, v(a), x) == x} says v(a) == x when ok
907def fv(ok: Bool, +y: Nat, +x: Nat) -> Nat:
908  match ok:
909    case True{}:
910      y
911    case False{}:
912      x
913
914# md: every value >= 1, or every value <= 1 (the base 0 case)
915def mode(md: Bool, +x: Nat) -> Bool:
916  match md:
917    case True{}:
918      Nat.is_le(1n, x)
919    case False{}:
920      Nat.is_le(x, 1n)
921
922def small_fits(+x: Nat, +h: {Nat.is_le(x, 1n) == True{} : Bool}) -> {C.fits(32n, x) == True{} : Bool}:
923  match x:
924    case 0n:
925      {==}
926    case 1n:
927      {==}
928    case 2n+y:
929      Empty.absurd({C.fits(32n, 2n+y) == True{} : Bool}, true_ne_false(Equal.sym(Bool, False{}, True{}, h)))
930
931def small_mul(+x: Nat, +y: Nat, +hx: {Nat.is_le(x, 1n) == True{} : Bool}, +hy: {Nat.is_le(y, 1n) == True{} : Bool}) -> {Nat.is_le(Nat.mul(x, y), 1n) == True{} : Bool}:
932  match x:
933    case 0n:
934      {==}
935    case 1n:
936      L.subst(Nat, z => {Nat.is_le(z, 1n) == True{} : Bool}, y, Nat.add(y, 0n), Equal.sym(Nat, Nat.add(y, 0n), y, N.add_zero(y)), hy)
937    case 2n+z:
938      Empty.absurd({Nat.is_le(Nat.mul(2n+z, y), 1n) == True{} : Bool}, true_ne_false(Equal.sym(Bool, False{}, True{}, hx)))
939
940def pos_of(+x: Nat, +h: {Nat.is_le(1n, x) == True{} : Bool}) -> {Nat.is_lt(0n, x) == True{} : Bool}:
941  match x:
942    case 0n:
943      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, true_ne_false(Equal.sym(Bool, False{}, True{}, h)))
944    case 1n+y:
945      {==}
946
947# x unfit, 1 <= y: x y unfit
948def unfit_mul(+x: Nat, +y: Nat, +hx: {C.fits(32n, x) == False{} : Bool}, +hy: {Nat.is_le(1n, y) == True{} : Bool}) -> {C.fits(32n, Nat.mul(x, y)) == False{} : Bool}:
949  unfit_mono(32n, x, Nat.mul(x, y), RT.le_mul_pos(x, y, pos_of(y, hy)), hx)
950
951def unfit_mul_r(+x: Nat, +y: Nat, +hy: {C.fits(32n, y) == False{} : Bool}, +hx: {Nat.is_le(1n, x) == True{} : Bool}) -> {C.fits(32n, Nat.mul(x, y)) == False{} : Bool}:
952  L.subst(Nat, z => {C.fits(32n, z) == False{} : Bool}, Nat.mul(y, x), Nat.mul(x, y), NA.mul_comm(y, x), unfit_mul(y, x, hy, hx))
953
954# an unfit value is >= 1, so the mode is the >= 1 one
955def unfit_big(+x: Nat, +md: Bool, +hm: {mode(md, x) == True{} : Bool}, +hx: {C.fits(32n, x) == False{} : Bool}) -> {md == True{} : Bool}:
956  match md:
957    case True{}:
958      {==}
959    case False{}:
960      Empty.absurd({False{} == True{} : Bool}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, x), False{}, Equal.sym(Bool, C.fits(32n, x), True{}, small_fits(x, hm)), hx)))
961
962def fv_mul(+a: U32, +x: U32, +n: Nat, +hn: {Nat.mul(v(a), v(x)) == n : Nat}, +c: Bool, +hc: {C.fits(32n, n) == c : Bool}) -> {fv(Bool.not(I.u32_is(NM.MulOver{a, x})), v(I.u32_op(NM.Mul{a, x})), n) == n : Nat}:
963  match c:
964    case True{}:
965      +hmo = mo_of(a, x, n, hn, True{}, hc)
966      %Equal.sym(Bool, I.u32_is(NM.MulOver{a, x}), False{}, hmo) : {fv(Bool.not(_), v(I.u32_op(NM.Mul{a, x})), n) == n : Nat}
967      Equal.trans(Nat, v(I.u32_op(NM.Mul{a, x})), Nat.mul(v(a), v(x)), n, LW.ops_mul(a, x, hmo), hn)
968    case False{}:
969      %Equal.sym(Bool, I.u32_is(NM.MulOver{a, x}), True{}, mo_of(a, x, n, hn, False{}, hc)) : {fv(Bool.not(_), v(I.u32_op(NM.Mul{a, x})), n) == n : Nat}
970      {==}
971
972# -- the squared base --
973
974def sq_fits(+more: Bool, +b: U32, +bok: Bool, +nb: Nat, +md: Bool, +hB: {C.fits(32n, nb) == bok : Bool}, +hb: {fv(bok, v(b), nb) == nb : Nat}, +hm: {mode(md, nb) == True{} : Bool}) -> {C.fits(32n, NF.sqn(more, nb)) == G.sq_ok(~U32, ~I.u32_is, more, b, bok) : Bool}:
975  match more bok:
976    case False{} _:
977      hB
978    case True{} True{}:
979      ok_mul(b, b, Nat.mul(nb, nb), nmul(v(b), v(b), nb, nb, hb, hb))
980    case True{} False{}:
981      +md1 = unfit_big(nb, md, hm, hB)
982      +h1 = L.subst(Bool, t => {mode(t, nb) == True{} : Bool}, md, True{}, md1, hm)
983      unfit_mul(nb, nb, hB, h1)
984
985def sq_fv(+more: Bool, +b: U32, +bok: Bool, +nb: Nat, +hb: {fv(bok, v(b), nb) == nb : Nat}) -> {fv(G.sq_ok(~U32, ~I.u32_is, more, b, bok), v(G.sq_val(~U32, ~I.u32_op, more, b)), NF.sqn(more, nb)) == NF.sqn(more, nb) : Nat}:
986  match more bok:
987    case False{} _:
988      hb
989    case True{} True{}:
990      fv_mul(b, b, Nat.mul(nb, nb), nmul(v(b), v(b), nb, nb, hb, hb), C.fits(32n, Nat.mul(nb, nb)), {==})
991    case True{} False{}:
992      {==}
993
994def sq_mode(+more: Bool, +nb: Nat, +md: Bool, +hm: {mode(md, nb) == True{} : Bool}) -> {mode(md, NF.sqn(more, nb)) == True{} : Bool}:
995  match more md:
996    case False{} _:
997      hm
998    case True{} True{}:
999      N.le_trans(1n, nb, Nat.mul(nb, nb), hm, RT.le_mul_pos(nb, nb, pos_of(nb, hm)))
1000    case True{} False{}:
1001      small_mul(nb, nb, hm, hm)
1002
1003# -- the accumulator --
1004
1005def ms_a(bit: Bool, +a: U32, +b: U32) -> U32:
1006  match bit:
1007    case True{}:
1008      I.u32_op(NM.Mul{a, b})
1009    case False{}:
1010      a
1011
1012def ms_ok(bit: Bool, +a: U32, +aok: Bool, +b: U32, +bok: Bool) -> Bool:
1013  match bit:
1014    case True{}:
1015      Bool.and(Bool.and(aok, bok), Bool.not(I.u32_is(NM.MulOver{a, b})))
1016    case False{}:
1017      aok
1018
1019def ms_eq(+bit: Bool, +b: U32, +bok: Bool, +a: U32, +aok: Bool) -> {G.mul_st(~U32, ~I.u32_op, ~I.u32_is, bit, b, bok, (a, aok)) == (ms_a(bit, a, b), ms_ok(bit, a, aok, b, bok)) : U32 & Bool}:
1020  match bit:
1021    case True{}:
1022      {==}
1023    case False{}:
1024      {==}
1025
1026def ms_fits(+bit: Bool, +a: U32, +aok: Bool, +b: U32, +bok: Bool, +na: Nat, +nb: Nat, +md: Bool, +hA: {C.fits(32n, na) == aok : Bool}, +ha: {fv(aok, v(a), na) == na : Nat}, +hma: {mode(md, na) == True{} : Bool}, +hB: {C.fits(32n, nb) == bok : Bool}, +hb: {fv(bok, v(b), nb) == nb : Nat}, +hmb: {mode(md, nb) == True{} : Bool}) -> {C.fits(32n, NF.msn(bit, na, nb)) == ms_ok(bit, a, aok, b, bok) : Bool}:
1027  match bit aok bok:
1028    case False{} _ _:
1029      hA
1030    case True{} True{} True{}:
1031      ok_mul(a, b, Nat.mul(na, nb), nmul(v(a), v(b), na, nb, ha, hb))
1032    case True{} False{} _:
1033      +md1 = unfit_big(na, md, hma, hA)
1034      unfit_mul(na, nb, hA, L.subst(Bool, t => {mode(t, nb) == True{} : Bool}, md, True{}, md1, hmb))
1035    case True{} True{} False{}:
1036      +md1 = unfit_big(nb, md, hmb, hB)
1037      unfit_mul_r(na, nb, hB, L.subst(Bool, t => {mode(t, na) == True{} : Bool}, md, True{}, md1, hma))
1038
1039def ms_fv(+bit: Bool, +a: U32, +aok: Bool, +b: U32, +bok: Bool, +na: Nat, +nb: Nat, +ha: {fv(aok, v(a), na) == na : Nat}, +hb: {fv(bok, v(b), nb) == nb : Nat}) -> {fv(ms_ok(bit, a, aok, b, bok), v(ms_a(bit, a, b)), NF.msn(bit, na, nb)) == NF.msn(bit, na, nb) : Nat}:
1040  match bit aok bok:
1041    case False{} _ _:
1042      ha
1043    case True{} True{} True{}:
1044      fv_mul(a, b, Nat.mul(na, nb), nmul(v(a), v(b), na, nb, ha, hb), C.fits(32n, Nat.mul(na, nb)), {==})
1045    case True{} False{} _:
1046      {==}
1047    case True{} True{} False{}:
1048      {==}
1049
1050def ms_mode(+bit: Bool, +na: Nat, +nb: Nat, +md: Bool, +hma: {mode(md, na) == True{} : Bool}, +hmb: {mode(md, nb) == True{} : Bool}) -> {mode(md, NF.msn(bit, na, nb)) == True{} : Bool}:
1051  match bit md:
1052    case False{} _:
1053      hma
1054    case True{} True{}:
1055      N.le_trans(1n, na, Nat.mul(na, nb), hma, RT.le_mul_pos(na, nb, pos_of(nb, hmb)))
1056    case True{} False{}:
1057      small_mul(na, nb, hma, hmb)
1058
1059def pw_fin(+a: U32, +aok: Bool, +na: Nat, +t0: Nat, +ct: Bool, +hA: {C.fits(32n, na) == aok : Bool}, +ha: {fv(aok, v(a), na) == na : Nat}, +et: {na == t0 : Nat}, +hct: {C.fits(32n, t0) == ct : Bool}) -> {G.fits(U32, Bool.not(aok), a) == G.fits(U32, Bool.not(ct), of(t0)) : Maybe<&2, U32>}:
1060  match aok ct:
1061    case True{} True{}:
1062      Equal.cong(U32, Maybe<&2, U32>, t => Some{t}, a, of(t0), as_of(a, t0, Equal.trans(Nat, v(a), na, t0, ha, et)))
1063    case False{} False{}:
1064      {==}
1065    case True{} False{}:
1066      Empty.absurd({G.fits(U32, Bool.not(True{}), a) == G.fits(U32, Bool.not(False{}), of(t0)) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, na), False{}, Equal.sym(Bool, C.fits(32n, na), True{}, hA), Equal.trans(Bool, C.fits(32n, na), C.fits(32n, t0), False{}, Equal.cong(Nat, Bool, t => C.fits(32n, t), na, t0, et), hct))))
1067    case False{} True{}:
1068      Empty.absurd({G.fits(U32, Bool.not(False{}), a) == G.fits(U32, Bool.not(True{}), of(t0)) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, t0), False{}, Equal.sym(Bool, C.fits(32n, t0), True{}, hct), Equal.trans(Bool, C.fits(32n, t0), C.fits(32n, na), False{}, Equal.cong(Nat, Bool, t => C.fits(32n, t), t0, na, Equal.sym(Nat, na, t0, et)), hA))))
1069
1070def powsim(+f: Nat, +e: Nat, +b: U32, +bok: Bool, +a: U32, +aok: Bool, +nb: Nat, +na: Nat, +t0: Nat, +md: Bool, +ct: Bool, +he: {Nat.is_le(e, f) == True{} : Bool}, +hB: {C.fits(32n, nb) == bok : Bool}, +hb: {fv(bok, v(b), nb) == nb : Nat}, +hmb: {mode(md, nb) == True{} : Bool}, +hA: {C.fits(32n, na) == aok : Bool}, +ha: {fv(aok, v(a), na) == na : Nat}, +hma: {mode(md, na) == True{} : Bool}, +ht: {Nat.mul(na, Nat.pow(nb, e)) == t0 : Nat}, +hct: {C.fits(32n, t0) == ct : Bool}) -> {G.pow_go(~U32, ~I.u32_op, ~I.u32_is, f, e, b, bok, (a, aok)) == G.fits(U32, Bool.not(ct), of(t0)) : Maybe<&2, U32>}:
1071  match f e:
1072    case 0n 0n:
1073      pw_fin(a, aok, na, t0, ct, hA, ha, Equal.trans(Nat, na, Nat.mul(na, 1n), t0, Equal.sym(Nat, Nat.mul(na, 1n), na, NA.mul_one(na)), ht), hct)
1074    case 0n 1n+j:
1075      Empty.absurd({G.pow_go(~U32, ~I.u32_op, ~I.u32_is, 0n, 1n+j, b, bok, (a, aok)) == G.fits(U32, Bool.not(ct), of(t0)) : Maybe<&2, U32>}, true_ne_false(Equal.sym(Bool, False{}, True{}, he)))
1076    case 1n+g 0n:
1077      pw_fin(a, aok, na, t0, ct, hA, ha, Equal.trans(Nat, na, Nat.mul(na, 1n), t0, Equal.sym(Nat, Nat.mul(na, 1n), na, NA.mul_one(na)), ht), hct)
1078    case 1n+ +g 1n+ +j:
1079      +more = Nat.is_lt(1n, 1n+j)
1080      +bit = Nat.is_eq(Nat.mod(1n+j, 2n), 1n)
1081      +e2 = Nat.div(1n+j, 2n)
1082      +ht2 = Equal.trans(Nat, Nat.mul(NF.msn(bit, na, nb), Nat.pow(NF.sqn(more, nb), e2)), Nat.mul(na, Nat.pow(nb, 1n+j)), t0, NF.powstep(j, na, nb), ht)
1083      +he2 = N.le_trans(e2, j, g, NF.half_le(j), he)
1084      +ih = powsim(g, e2, G.sq_val(~U32, ~I.u32_op, more, b), G.sq_ok(~U32, ~I.u32_is, more, b, bok), ms_a(bit, a, b), ms_ok(bit, a, aok, b, bok), NF.sqn(more, nb), NF.msn(bit, na, nb), t0, md, ct, he2, sq_fits(more, b, bok, nb, md, hB, hb, hmb), sq_fv(more, b, bok, nb, hb), sq_mode(more, nb, md, hmb), ms_fits(bit, a, aok, b, bok, na, nb, md, hA, ha, hma, hB, hb, hmb), ms_fv(bit, a, aok, b, bok, na, nb, ha, hb), ms_mode(bit, na, nb, md, hma, hmb), ht2, hct)
1085      L.subst(U32 & Bool, z => {G.pow_go(~U32, ~I.u32_op, ~I.u32_is, g, e2, G.sq_val(~U32, ~I.u32_op, more, b), G.sq_ok(~U32, ~I.u32_is, more, b, bok), z) == G.fits(U32, Bool.not(ct), of(t0)) : Maybe<&2, U32>}, (ms_a(bit, a, b), ms_ok(bit, a, aok, b, bok)), G.mul_st(~U32, ~I.u32_op, ~I.u32_is, bit, b, bok, (a, aok)), Equal.sym(U32 & Bool, G.mul_st(~U32, ~I.u32_op, ~I.u32_is, bit, b, bok, (a, aok)), (ms_a(bit, a, b), ms_ok(bit, a, aok, b, bok)), ms_eq(bit, b, bok, a, aok)), ih)
1086
1087def md_init(+x: Nat) -> {mode(Nat.is_le(1n, x), x) == True{} : Bool} & {mode(Nat.is_le(1n, x), 1n) == True{} : Bool}:
1088  match x:
1089    case 0n:
1090      ({==}, {==})
1091    case 1n+y:
1092      +ez = Equal.sym(Bool, Nat.is_le(0n, y), True{}, N.zero_le(y))
1093      (L.subst(Bool, t => {mode(t, 1n+y) == True{} : Bool}, True{}, Nat.is_le(0n, y), ez, N.zero_le(y)), L.subst(Bool, t => {mode(t, 1n) == True{} : Bool}, True{}, Nat.is_le(0n, y), ez, {==}))
1094
1095def pow_fin(+x: U32, +k: Nat, p: {mode(Nat.is_le(1n, v(x)), v(x)) == True{} : Bool} & {mode(Nat.is_le(1n, v(x)), 1n) == True{} : Bool}) -> SG.Pow.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, x, k):
1096  (+hmb, +hma) = p
1097  +one = I.u32_op(NM.One{})
1098  +t0 = Nat.pow(v(x), k)
1099  +ht = Equal.trans(Nat, Nat.mul(1n, t0), Nat.add(t0, 0n), t0, {==}, N.add_zero(t0))
1100  +s = powsim(1n+k, k, x, True{}, one, True{}, v(x), 1n, t0, Nat.is_le(1n, v(x)), C.fits(32n, t0), N.le_succ(k), LW.vb(x), {==}, hmb, {==}, one_v(), hma, ht, {==})
1101  +g = G.pow_go(~U32, ~I.u32_op, ~I.u32_is, 1n+k, k, x, True{}, (one, True{}))
1102  Equal.trans(Result<&2, &2, NM.NumError, U32>, G.ok(U32, g), G.ok(U32, G.fits(U32, Bool.not(C.fits(32n, t0)), of(t0))), SG.checked(~U32, ~SG.u32_of, 32n, t0), Equal.cong(Maybe<&2, U32>, Result<&2, &2, NM.NumError, U32>, t => G.ok(U32, t), g, G.fits(U32, Bool.not(C.fits(32n, t0)), of(t0)), s), okfits(t0, C.fits(32n, t0)))
1103
1104def pow_checked(+x: U32, +k: Nat) -> SG.Pow.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, x, k):
1105  pow_fin(x, k, md_init(v(x)))
1106
1107# ---- iroot: bisection with lo <= R < lo + w, the width halving ----
1108
1109def pw_val(+x: U32, +k: Nat, p: {mode(Nat.is_le(1n, v(x)), v(x)) == True{} : Bool} & {mode(Nat.is_le(1n, v(x)), 1n) == True{} : Bool}) -> {G.pow_go(~U32, ~I.u32_op, ~I.u32_is, 1n+k, k, x, True{}, (I.u32_op(NM.One{}), True{})) == G.fits(U32, Bool.not(C.fits(32n, Nat.pow(v(x), k))), of(Nat.pow(v(x), k))) : Maybe<&2, U32>}:
1110  (+hmb, +hma) = p
1111  +t0 = Nat.pow(v(x), k)
1112  +ht = Equal.trans(Nat, Nat.mul(1n, t0), Nat.add(t0, 0n), t0, {==}, N.add_zero(t0))
1113  powsim(1n+k, k, x, True{}, I.u32_op(NM.One{}), True{}, v(x), 1n, t0, Nat.is_le(1n, v(x)), C.fits(32n, t0), N.le_succ(k), LW.vb(x), {==}, hmb, {==}, one_v(), hma, ht, {==})
1114
1115def rlf(+K: Nat, +hK: {K == 32n : Nat}, +n: U32, +P: Nat, +c: Bool, +hc: {C.fits(32n, P) == c : Bool}) -> {G.root_le_fin(~U32, ~I.u32_op, ~I.u32_is, n, G.fits(U32, Bool.not(c), of(P))) == Nat.is_le(P, v(n)) : Bool}:
1116  match c:
1117    case True{}:
1118      lev(of(P), n, P, v(n), LW.vo(P, hc), {==})
1119    case False{}:
1120      +h1 = L.subst(Nat, z => {C.fits(z, P) == False{} : Bool}, 32n, K, Equal.sym(Nat, K, 32n, hK), hc)
1121      +h2 = Equal.trans(Bool, Nat.is_lt(P, C.pow2(K)), C.fits(K, P), False{}, Equal.sym(Bool, C.fits(K, P), Nat.is_lt(P, C.pow2(K)), WW.fits_lt(K, P)), h1)
1122      +hn = N.lt_le_trans(v(n), C.pow2(K), P, U32P.val_lt(1n, {==}, K, hK, n), N.not_lt_le(P, C.pow2(K), h2))
1123      Equal.sym(Bool, Nat.is_le(P, v(n)), False{}, N.lt_not_le(v(n), P, hn))
1124
1125def rl_v(+K: Nat, +hK: {K == 32n : Nat}, +n: U32, +k: Nat, +r: U32) -> {G.root_le(~U32, ~I.u32_op, ~I.u32_is, n, k, r) == Nat.is_le(Nat.pow(v(r), k), v(n)) : Bool}:
1126  +P = Nat.pow(v(r), k)
1127  Equal.trans(Bool, G.root_le_fin(~U32, ~I.u32_op, ~I.u32_is, n, G.pow_go(~U32, ~I.u32_op, ~I.u32_is, 1n+k, k, r, True{}, (I.u32_op(NM.One{}), True{}))), G.root_le_fin(~U32, ~I.u32_op, ~I.u32_is, n, G.fits(U32, Bool.not(C.fits(32n, P)), of(P))), Nat.is_le(P, v(n)), Equal.cong(Maybe<&2, U32>, Bool, t => G.root_le_fin(~U32, ~I.u32_op, ~I.u32_is, n, t), G.pow_go(~U32, ~I.u32_op, ~I.u32_is, 1n+k, k, r, True{}, (I.u32_op(NM.One{}), True{})), G.fits(U32, Bool.not(C.fits(32n, P)), of(P)), pw_val(r, k, md_init(v(r)))), rlf(K, hK, n, P, C.fits(32n, P), {==}))
1128
1129def imid_v(+K: Nat, +hK: {K == 32n : Nat}, +lo: U32, +hi: U32, +a: Nat, +w: Nat, +ha: {v(lo) == a : Nat}, +hh: {v(hi) == Nat.add(a, w) : Nat}) -> {v(G.imid(~U32, ~I.u32_op, lo, hi)) == Nat.add(a, Nat.div(w, 2n)) : Nat}:
1130  +s = I.u32_op(NM.Sub{hi, lo})
1131  +es = Equal.trans(Nat, v(s), Nat.sub(v(hi), v(lo)), w, LW.ops_sub(hi, lo, le_v(lo, hi, a, Nat.add(a, w), ha, hh, N.le_add_right(a, w))), Equal.trans(Nat, Nat.sub(v(hi), v(lo)), Nat.sub(Nat.add(a, w), a), w, nsub(v(hi), v(lo), Nat.add(a, w), a, hh, ha), N.add_sub_cancel(a, w)))
1132  +h = I.u32_op(NM.Half{s})
1133  +eh = Equal.trans(Nat, v(h), Nat.div(v(s), 2n), Nat.div(w, 2n), LW.ops_half(s), Equal.cong(Nat, Nat, t => Nat.div(t, 2n), v(s), w, es))
1134  +sum = Nat.add(a, Nat.div(w, 2n))
1135  +esum = nadd(v(lo), v(h), a, Nat.div(w, 2n), ha, eh)
1136  +hle = N.le_add_left(Nat.div(w, 2n), w, a, AR2.div_le(w, 2n))
1137  +hhk = L.subst(Nat, z => {Nat.is_lt(z, C.pow2(K)) == True{} : Bool}, v(hi), Nat.add(a, w), hh, U32P.val_lt(1n, {==}, K, hK, hi))
1138  +hfit = fits32(K, hK, sum, N.le_lt_trans(sum, Nat.add(a, w), C.pow2(K), hle, hhk))
1139  Equal.trans(Nat, v(I.u32_op(NM.Add{lo, h})), Nat.add(v(lo), v(h)), sum, LW.ops_add(lo, h, ao_of(lo, h, sum, esum, True{}, hfit)), esum)
1140
1141def lt_add_r(+a: Nat, +q: Nat, +h: {Nat.is_lt(0n, q) == True{} : Bool}) -> {Nat.is_lt(a, Nat.add(a, q)) == True{} : Bool}:
1142  +h1 = Equal.trans(Bool, Nat.is_lt(Nat.add(a, 0n), Nat.add(a, q)), Nat.is_lt(0n, q), True{}, NF.lt_add_cancel(a, 0n, q), h)
1143  L.subst(Nat, z => {Nat.is_lt(z, Nat.add(a, q)) == True{} : Bool}, Nat.add(a, 0n), a, N.add_zero(a), h1)
1144
1145# inc(lo) < lo + w as 1 < w
1146def more_v(+K: Nat, +hK: {K == 32n : Nat}, +lo: U32, +hi: U32, +a: Nat, +w: Nat, +ha: {v(lo) == a : Nat}, +hh: {v(hi) == Nat.add(a, w) : Nat}, +hw: {Nat.is_lt(0n, w) == True{} : Bool}) -> {I.u32_is(NM.Lt{G.inc(~U32, ~I.u32_op, lo), hi}) == Nat.is_lt(1n, w) : Bool}:
1147  +ei = inc_v(K, hK, lo, hi, a, Nat.add(a, w), ha, hh, lt_add_r(a, w, hw))
1148  Equal.trans(Bool, I.u32_is(NM.Lt{G.inc(~U32, ~I.u32_op, lo), hi}), Nat.is_lt(1n+a, Nat.add(a, w)), Nat.is_lt(1n, w), ltv(G.inc(~U32, ~I.u32_op, lo), hi, 1n+a, Nat.add(a, w), ei, hh), L.subst(Nat, z => {Nat.is_lt(z, Nat.add(a, w)) == Nat.is_lt(1n, w) : Bool}, Nat.add(a, 1n), 1n+a, plus1(a), NF.lt_add_cancel(a, 1n, w)))
1149
1150def srch(+f: Nat, +n: U32, +k: Nat, +lo: U32, +hi: U32, +m: U32, +more: Bool, +hit: Bool, +j: Nat, +nlo: Nat, +w: Nat, +R: Nat, +K: Nat, +hK: {K == 32n : Nat}, +hlo: {v(lo) == nlo : Nat}, +hhi: {v(hi) == Nat.add(nlo, w) : Nat}, +hm: {v(m) == Nat.add(nlo, Nat.div(w, 2n)) : Nat}, +hR1: {Nat.is_le(Nat.pow(R, k), v(n)) == True{} : Bool}, +hR2: {Nat.is_lt(v(n), Nat.pow(1n+R, k)) == True{} : Bool}, +hl: {Nat.is_le(nlo, R) == True{} : Bool}, +hr: {Nat.is_lt(R, Nat.add(nlo, w)) == True{} : Bool}, +hmore: {more == Nat.is_lt(1n, w) : Bool}, +hhit: {hit == Nat.is_le(Nat.pow(Nat.add(nlo, Nat.div(w, 2n)), k), v(n)) : Bool}, +hw: {Nat.is_le(w, C.pow2(j)) == True{} : Bool}, +hf: {Nat.is_le(1n+j, f) == True{} : Bool}) -> {v(G.search_go(~U32, ~I.u32_op, ~I.u32_is, f, n, k, lo, hi, m, more, hit)) == R : Nat}:
1151  match f more hit j:
1152    case 0n _ _ _:
1153      Empty.absurd({v(G.search_go(~U32, ~I.u32_op, ~I.u32_is, 0n, n, k, lo, hi, m, more, hit)) == R : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, hf)))
1154    case 1n+g False{} _ _:
1155      +hw1 = N.not_lt_le(1n, w, Equal.sym(Bool, False{}, Nat.is_lt(1n, w), hmore))
1156      +h1 = L.subst(Nat, z => {Nat.is_le(Nat.add(nlo, w), z) == True{} : Bool}, Nat.add(nlo, 1n), 1n+nlo, plus1(nlo), N.le_add_left(w, 1n, nlo, hw1))
1157      +hrl = N.lt_succ_le(R, nlo, N.lt_le_trans(R, Nat.add(nlo, w), 1n+nlo, hr, h1))
1158      Equal.trans(Nat, v(lo), nlo, R, hlo, N.le_antisym(nlo, R, hl, hrl))
1159    case 1n+g True{} _ 0n:
1160      Empty.absurd({v(G.search_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, n, k, lo, hi, m, True{}, hit)) == R : Nat}, true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(1n, w), False{}, hmore, N.le_not_lt(1n, w, hw))))
1161    case 1n+ +g True{} True{} 1n+ +jp:
1162      +q = Nat.div(w, 2n)
1163      +X = Nat.add(nlo, q)
1164      +w2 = Nat.sub(w, q)
1165      +hqw = Equal.trans(Nat, Nat.add(q, w2), w, w, N.sub_add(w, q, AR2.div_le(w, 2n)), {==})
1166      +ehi = Equal.trans(Nat, Nat.add(X, w2), Nat.add(nlo, Nat.add(q, w2)), Nat.add(nlo, w), N.add_assoc(nlo, q, w2), Equal.cong(Nat, Nat, t => Nat.add(nlo, t), Nat.add(q, w2), w, hqw))
1167      +hhi2 = Equal.trans(Nat, v(hi), Nat.add(nlo, w), Nat.add(X, w2), hhi, Equal.sym(Nat, Nat.add(X, w2), Nat.add(nlo, w), ehi))
1168      +hw0 = N.lt_trans(0n, 1n, w, {==}, Equal.sym(Bool, True{}, Nat.is_lt(1n, w), hmore))
1169      +hdw = L.subst(Nat, z => {Nat.is_lt(w, z) == True{} : Bool}, Nat.add(w, w), Nat.double(w), Equal.sym(Nat, Nat.double(w), Nat.add(w, w), NA.double_self(w)), lt_add_r(w, w, hw0))
1170      +hpos = RT.sub_pos(q, w, NF.half_below(w, w, hdw))
1171      +m2 = G.imid(~U32, ~I.u32_op, m, hi)
1172      +hm2 = imid_v(K, hK, m, hi, X, w2, hm, hhi2)
1173      +hmore2 = more_v(K, hK, m, hi, X, w2, hm, hhi2, hpos)
1174      +hhit2 = Equal.trans(Bool, G.root_le(~U32, ~I.u32_op, ~I.u32_is, n, k, m2), Nat.is_le(Nat.pow(v(m2), k), v(n)), Nat.is_le(Nat.pow(Nat.add(X, Nat.div(w2, 2n)), k), v(n)), rl_v(K, hK, n, k, m2), Equal.cong(Nat, Bool, t => Nat.is_le(Nat.pow(t, k), v(n)), v(m2), Nat.add(X, Nat.div(w2, 2n)), hm2))
1175      +hl2 = NF.root_below(R, X, k, v(n), Equal.sym(Bool, True{}, Nat.is_le(Nat.pow(X, k), v(n)), hhit), hR2)
1176      +hr2 = L.subst(Nat, z => {Nat.is_lt(R, z) == True{} : Bool}, Nat.add(nlo, w), Nat.add(X, w2), Equal.sym(Nat, Nat.add(X, w2), Nat.add(nlo, w), ehi), hr)
1177      +hw3 = NF.w_hi(w, C.pow2(jp), hw)
1178      srch(g, n, k, m, hi, m2, I.u32_is(NM.Lt{G.inc(~U32, ~I.u32_op, m), hi}), G.root_le(~U32, ~I.u32_op, ~I.u32_is, n, k, m2), jp, X, w2, R, K, hK, hm, hhi2, hm2, hR1, hR2, hl2, hr2, Equal.sym(Bool, Nat.is_lt(1n, w2), I.u32_is(NM.Lt{G.inc(~U32, ~I.u32_op, m), hi}), Equal.sym(Bool, I.u32_is(NM.Lt{G.inc(~U32, ~I.u32_op, m), hi}), Nat.is_lt(1n, w2), hmore2)), hhit2, hw3, hf)
1179    case 1n+ +g True{} False{} 1n+ +jp:
1180      +q = Nat.div(w, 2n)
1181      +X = Nat.add(nlo, q)
1182      +h2w = N.lt_succ_le_succ(1n, w, Equal.sym(Bool, True{}, Nat.is_lt(1n, w), hmore))
1183      +hq1 = Equal.trans(Bool, Nat.is_le(1n, q), Nat.is_le(Nat.mul(1n, 2n), w), True{}, NR.le_div(1n, 1n, w), h2w)
1184      +hpos = pos_of(q, hq1)
1185      +m2 = G.imid(~U32, ~I.u32_op, lo, m)
1186      +hm2 = imid_v(K, hK, lo, m, nlo, q, hlo, hm)
1187      +hmore2 = more_v(K, hK, lo, m, nlo, q, hlo, hm, hpos)
1188      +hhit2 = Equal.trans(Bool, G.root_le(~U32, ~I.u32_op, ~I.u32_is, n, k, m2), Nat.is_le(Nat.pow(v(m2), k), v(n)), Nat.is_le(Nat.pow(Nat.add(nlo, Nat.div(q, 2n)), k), v(n)), rl_v(K, hK, n, k, m2), Equal.cong(Nat, Bool, t => Nat.is_le(Nat.pow(t, k), v(n)), v(m2), Nat.add(nlo, Nat.div(q, 2n)), hm2))
1189      +hr2 = NF.root_above(R, X, k, v(n), Equal.sym(Bool, False{}, Nat.is_le(Nat.pow(X, k), v(n)), hhit), hR1)
1190      +hw3 = NF.w_lo(w, C.pow2(jp), hw)
1191      srch(g, n, k, lo, m, m2, I.u32_is(NM.Lt{G.inc(~U32, ~I.u32_op, lo), m}), G.root_le(~U32, ~I.u32_op, ~I.u32_is, n, k, m2), jp, nlo, q, R, K, hK, hlo, hm, hm2, hR1, hR2, hl, hr2, Equal.sym(Bool, Nat.is_lt(1n, q), I.u32_is(NM.Lt{G.inc(~U32, ~I.u32_op, lo), m}), Equal.sym(Bool, I.u32_is(NM.Lt{G.inc(~U32, ~I.u32_op, lo), m}), Nat.is_lt(1n, q), hmore2)), hhit2, hw3, hf)
1192
1193def iroot_big(+K: Nat, +hK: {K == 32n : Nat}, +n: U32, +kp: Nat) -> {v(G.iroot_k(~U32, ~I.u32_op, ~I.u32_is, n, 2n+kp)) == M.iroot_k(v(n), 2n+kp) : Nat}:
1194  +bg = G.bit_length(~U32, ~I.u32_op, ~I.u32_is, n)
1195  +bl = M.bit_length(v(n))
1196  +ebl = bit_length_k(K, hK, n)
1197  +hn = U32P.val_lt(1n, {==}, K, hK, n)
1198  +hbl = L.subst(Nat, z => {Nat.is_le(bl, z) == True{} : Bool}, K, 32n, hK, NF.bl_le_n(K, v(n), hn))
1199  +E2 = {1n+Nat.div(bl, 2n+kp) : Nat}
1200  +E = {1n+Nat.div(bg, 2n+kp) : Nat}
1201  +eE = Equal.cong(Nat, Nat, t => 1n+Nat.div(t, 2n+kp), bg, bl, ebl)
1202  +hE2 = NF.e_lt(kp, bl, hbl)
1203  +hE = L.subst(Nat, z => {Nat.is_lt(z, 32n) == True{} : Bool}, E2, E, Equal.sym(Nat, E, E2, eE), hE2)
1204  +hi = I.u32_op(NM.Pow2{E})
1205  +W = C.pow2(E2)
1206  ehi0 = LW.ops_pow2(E, hE)
1207  +ehi = Equal.trans(Nat, v(hi), C.pow2(E), W, ehi0, Equal.cong(Nat, Nat, t => C.pow2(t), E, E2, eE))
1208  +zero = I.u32_op(NM.ZeroOp{})
1209  +m = G.imid(~U32, ~I.u32_op, zero, hi)
1210  +hm = imid_v(K, hK, zero, hi, 0n, W, zero_v(), ehi)
1211  +hmore = ltv(I.u32_op(NM.One{}), hi, 1n, W, one_v(), ehi)
1212  +hhit = Equal.trans(Bool, G.root_le(~U32, ~I.u32_op, ~I.u32_is, n, 2n+kp, m), Nat.is_le(Nat.pow(v(m), 2n+kp), v(n)), Nat.is_le(Nat.pow(Nat.div(W, 2n), 2n+kp), v(n)), rl_v(K, hK, n, 2n+kp, m), Equal.cong(Nat, Bool, t => Nat.is_le(Nat.pow(t, 2n+kp), v(n)), v(m), Nat.div(W, 2n), hm))
1213  +R = M.iroot_k(v(n), 2n+kp)
1214  +hb = Equal.trans(Bool, Nat.is_le(Nat.pow(P2.pow2t(E2), 2n+kp), v(n)), M.root_le(v(n), 2n+kp, P2.pow2t(E2)), False{}, Equal.sym(Bool, M.root_le(v(n), 2n+kp, P2.pow2t(E2)), Nat.is_le(Nat.pow(P2.pow2t(E2), 2n+kp), v(n)), RT.root_le_ok(v(n), 2n+kp, P2.pow2t(E2))), RT.hi_bound(v(n), 1n+kp))
1215  +hb2 = L.subst(Nat, z => {Nat.is_le(Nat.pow(z, 2n+kp), v(n)) == False{} : Bool}, P2.pow2t(E2), W, PP.same(E2), hb)
1216  +hR1 = RT.iroot_le(v(n), 1n+kp)
1217  +hr = NF.root_above(R, W, 2n+kp, v(n), hb2, hR1)
1218  +hf = N.le_trans(1n+E2, 32n, 140n, N.lt_succ_le_succ(E2, 32n, hE2), {==})
1219  srch(140n, n, 2n+kp, zero, hi, m, I.u32_is(NM.Lt{I.u32_op(NM.One{}), hi}), G.root_le(~U32, ~I.u32_op, ~I.u32_is, n, 2n+kp, m), E2, 0n, W, R, K, hK, zero_v(), ehi, hm, hR1, RT.lt_succ_iroot(v(n), 1n+kp), N.zero_le(R), hr, hmore, hhit, N.le_refl(W), hf)
1220
1221def iroot_agrees(+n: U32, +k: Nat) -> SG.Iroot.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, n, k):
1222  match k:
1223    case 0n:
1224      {==}
1225    case 1n:
1226      Equal.cong(U32, Result<&2, &2, NM.NumError, U32>, t => Done{t}, n, of(v(n)), as_of(n, v(n), {==}))
1227    case 2n+ +kp:
1228      Equal.cong(U32, Result<&2, &2, NM.NumError, U32>, t => Done{t}, G.iroot_k(~U32, ~I.u32_op, ~I.u32_is, n, 2n+kp), of(M.iroot_k(v(n), 2n+kp)), as_of(G.iroot_k(~U32, ~I.u32_op, ~I.u32_is, n, 2n+kp), M.iroot_k(v(n), 2n+kp), iroot_big(32n, {==}, n, kp)))
1229
1230# ---- comb: C(n, i + 1) = (r / g) ((n - i) / ((i + 1) / g)), g = gcd(r, i + 1) ----
1231
1232def nz_of(+x: U32, +n: Nat, +hx: {v(x) == n : Nat}, +h: {Nat.is_lt(0n, n) == True{} : Bool}) -> {Nat.is_eq(v(x), 0n) == False{} : Bool}:
1233  Equal.trans(Bool, Nat.is_eq(v(x), 0n), Nat.is_eq(n, 0n), False{}, Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(x), n, hx), N.is_eq_sym_false(0n, n, N.is_eq_lt(0n, n, h)))
1234
1235def ndiv(+a: Nat, +b: Nat, +na: Nat, +nb: Nat, +ha: {a == na : Nat}, +hb: {b == nb : Nat}) -> {Nat.div(a, b) == Nat.div(na, nb) : Nat}:
1236  Equal.trans(Nat, Nat.div(a, b), Nat.div(na, b), Nat.div(na, nb), Equal.cong(Nat, Nat, t => Nat.div(t, b), a, na, ha), Equal.cong(Nat, Nat, t => Nat.div(na, t), b, nb, hb))
1237
1238def quot_v(+a: U32, +b: U32, +na: Nat, +nb: Nat, +ha: {v(a) == na : Nat}, +hb: {v(b) == nb : Nat}, +hpos: {Nat.is_lt(0n, nb) == True{} : Bool}) -> {v(I.u32_op(NM.Quot{a, b})) == Nat.div(na, nb) : Nat}:
1239  Equal.trans(Nat, v(I.u32_op(NM.Quot{a, b})), Nat.div(v(a), v(b)), Nat.div(na, nb), LW.ops_quot(a, b, nz_of(b, nb, hb, hpos)), ndiv(v(a), v(b), na, nb, ha, hb))
1240
1241def combsim(+f: Nat, +n: U32, +i: U32, +k: U32, +r: U32, +nn: Nat, +ni: Nat, +k0: Nat, +K: Nat, +ok: Bool, +more: Bool, +cn: Bool, +hK: {K == 32n : Nat}, +hn: {v(n) == nn : Nat}, +hi: {v(i) == ni : Nat}, +hk: {v(k) == k0 : Nat}, +h2: {Nat.is_le(Nat.double(k0), nn) == True{} : Bool}, +hle: {Nat.is_le(ni, k0) == True{} : Bool}, +hf: {Nat.is_le(1n+K, Nat.add(f, ni)) == True{} : Bool}, +hok: {C.fits(32n, S.choose(nn, ni)) == ok : Bool}, +ha: {fv(ok, v(r), S.choose(nn, ni)) == S.choose(nn, ni) : Nat}, +hmore: {more == Nat.is_lt(ni, k0) : Bool}, +hcn: {C.fits(32n, S.choose(nn, k0)) == cn : Bool}) -> {G.comb_go(~U32, ~I.u32_op, ~I.u32_is, f, n, i, k, (r, ok), more) == G.fits(U32, Bool.not(cn), of(S.choose(nn, k0))) : Maybe<&2, U32>}:
1242  match f ok more cn:
1243    case 0n True{} _ _:
1244      +h2i = N.le_trans(Nat.double(ni), Nat.double(k0), nn, N.double_le(ni, k0, hle), h2)
1245      +big = CN.cbig(K, nn, ni, N.le_trans(K, 1n+K, ni, N.le_succ(K), hf), h2i)
1246      Empty.absurd({G.comb_go(~U32, ~I.u32_op, ~I.u32_is, 0n, n, i, k, (r, True{}), more) == G.fits(U32, Bool.not(cn), of(S.choose(nn, k0))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(S.choose(nn, ni), C.pow2(K)), False{}, Equal.sym(Bool, Nat.is_lt(S.choose(nn, ni), C.pow2(K)), True{}, fk(K, hK, S.choose(nn, ni), hok)), N.le_not_lt(S.choose(nn, ni), C.pow2(K), big))))
1247    case 0n False{} _ True{}:
1248      Empty.absurd({G.comb_go(~U32, ~I.u32_op, ~I.u32_is, 0n, n, i, k, (r, False{}), more) == G.fits(U32, Bool.not(True{}), of(S.choose(nn, k0))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, S.choose(nn, k0)), False{}, Equal.sym(Bool, C.fits(32n, S.choose(nn, k0)), True{}, hcn), unfit_mono(32n, S.choose(nn, ni), S.choose(nn, k0), CN.cmono(nn, ni, k0, hle, h2), hok))))
1249    case 0n False{} _ False{}:
1250      {==}
1251    case 1n+g False{} _ True{}:
1252      Empty.absurd({G.comb_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, n, i, k, (r, False{}), more) == G.fits(U32, Bool.not(True{}), of(S.choose(nn, k0))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, S.choose(nn, k0)), False{}, Equal.sym(Bool, C.fits(32n, S.choose(nn, k0)), True{}, hcn), unfit_mono(32n, S.choose(nn, ni), S.choose(nn, k0), CN.cmono(nn, ni, k0, hle, h2), hok))))
1253    case 1n+g False{} _ False{}:
1254      {==}
1255    case 1n+g True{} False{} True{}:
1256      +eik = N.le_antisym(ni, k0, hle, N.not_lt_le(ni, k0, Equal.sym(Bool, False{}, Nat.is_lt(ni, k0), hmore)))
1257      Equal.cong(U32, Maybe<&2, U32>, t => Some{t}, r, of(S.choose(nn, k0)), as_of(r, S.choose(nn, k0), Equal.trans(Nat, v(r), S.choose(nn, ni), S.choose(nn, k0), ha, Equal.cong(Nat, Nat, t => S.choose(nn, t), ni, k0, eik))))
1258    case 1n+g True{} False{} False{}:
1259      +eik = N.le_antisym(ni, k0, hle, N.not_lt_le(ni, k0, Equal.sym(Bool, False{}, Nat.is_lt(ni, k0), hmore)))
1260      Empty.absurd({G.comb_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, n, i, k, (r, True{}), False{}) == G.fits(U32, Bool.not(False{}), of(S.choose(nn, k0))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, S.choose(nn, ni)), False{}, Equal.sym(Bool, C.fits(32n, S.choose(nn, ni)), True{}, hok), Equal.trans(Bool, C.fits(32n, S.choose(nn, ni)), C.fits(32n, S.choose(nn, k0)), False{}, Equal.cong(Nat, Bool, t => C.fits(32n, S.choose(nn, t)), ni, k0, eik), hcn))))
1261    case 1n+ +g True{} True{} _:
1262      +hlt = Equal.sym(Bool, True{}, Nat.is_lt(ni, k0), hmore)
1263      +hin = N.le_trans(ni, k0, nn, N.lt_le(ni, k0, hlt), N.le_trans(k0, Nat.double(k0), nn, N.double_self_le(k0), h2))
1264      +x = G.inc(~U32, ~I.u32_op, i)
1265      +ex = inc_v(K, hK, i, k, ni, k0, hi, hk, hlt)
1266      +t = I.u32_op(NM.Sub{n, i})
1267      +tn = Nat.sub(nn, ni)
1268      +et = Equal.trans(Nat, v(t), Nat.sub(v(n), v(i)), tn, LW.ops_sub(n, i, le_v(i, n, ni, nn, hi, hn, hin)), nsub(v(n), v(i), nn, ni, hn, hi))
1269      +c = S.choose(nn, ni)
1270      +c1 = S.choose(nn, 1n+ni)
1271      +ce = FA.choose_succ_right(nn, ni)
1272      +gu = G.gcd(~U32, ~I.u32_op, ~I.u32_is, r, x)
1273      +eg = Equal.trans(Nat, v(gu), M.gcd(v(r), v(x)), CN.gg(c, ni), gcd_val(r, x), Equal.trans(Nat, M.gcd(v(r), v(x)), M.gcd(c, v(x)), M.gcd(c, 1n+ni), Equal.cong(Nat, Nat, z => M.gcd(z, v(x)), v(r), c, ha), Equal.cong(Nat, Nat, z => M.gcd(c, z), v(x), 1n+ni, ex)))
1274      +au = I.u32_op(NM.Quot{r, gu})
1275      +ea = Equal.trans(Nat, v(au), Nat.div(c, CN.gg(c, ni)), CN.wl(c, ni), quot_v(r, gu, c, CN.gg(c, ni), ha, eg, CN.g_pos(c, ni)), CN.div_c(c, ni))
1276      +ju = I.u32_op(NM.Quot{x, gu})
1277      +ej = Equal.trans(Nat, v(ju), Nat.div(1n+ni, CN.gg(c, ni)), CN.wr(c, ni), quot_v(x, gu, 1n+ni, CN.gg(c, ni), ex, eg, CN.g_pos(c, ni)), CN.div_j(c, ni))
1278      +bu = I.u32_op(NM.Quot{t, ju})
1279      +eb = Equal.trans(Nat, v(bu), Nat.div(tn, CN.wr(c, ni)), CN.sq(c, ni, tn, c1), quot_v(t, ju, tn, CN.wr(c, ni), et, ej, CN.wr_pos(c, ni)), CN.div_t(c, ni, tn, c1, ce))
1280      +hpn = Equal.trans(Nat, Nat.mul(v(au), v(bu)), Nat.mul(CN.wl(c, ni), CN.sq(c, ni, tn, c1)), c1, nmul(v(au), v(bu), CN.wl(c, ni), CN.sq(c, ni, tn, c1), ea, eb), CN.prod_eq(c, ni, tn, c1, ce))
1281      +hf2 = L.subst(Nat, z => {Nat.is_le(1n+K, z) == True{} : Bool}, 1n+Nat.add(g, ni), Nat.add(g, 1n+ni), Equal.sym(Nat, Nat.add(g, 1n+ni), 1n+Nat.add(g, ni), NA.add_succ(g, ni)), hf)
1282      combsim(g, n, x, k, I.u32_op(NM.Mul{au, bu}), nn, 1n+ni, k0, K, Bool.not(I.u32_is(NM.MulOver{au, bu})), I.u32_is(NM.Lt{x, k}), cn, hK, hn, ex, hk, h2, succ_le(ni, k0, hlt), hf2, ok_mul(au, bu, c1, hpn), fv_mul(au, bu, c1, hpn, C.fits(32n, c1), {==}), ltv(x, k, 1n+ni, k0, ex, hk), hcn)
1283
1284def min_le_a(+a: Nat, +b: Nat, +c: Bool, +hc: {Nat.is_lt(a, b) == c : Bool}) -> {Nat.is_le(Nat.min(a, b), a) == True{} : Bool}:
1285  match c:
1286    case True{}:
1287      L.subst(Nat, z => {Nat.is_le(z, a) == True{} : Bool}, a, Nat.min(a, b), Equal.sym(Nat, Nat.min(a, b), a, N.min_left(a, b, hc)), N.le_refl(a))
1288    case False{}:
1289      L.subst(Nat, z => {Nat.is_le(z, a) == True{} : Bool}, b, Nat.min(a, b), Equal.sym(Nat, Nat.min(a, b), b, N.min_right(a, b, hc)), N.not_lt_le(a, b, hc))
1290
1291def min_le_b(+a: Nat, +b: Nat, +c: Bool, +hc: {Nat.is_lt(a, b) == c : Bool}) -> {Nat.is_le(Nat.min(a, b), b) == True{} : Bool}:
1292  match c:
1293    case True{}:
1294      L.subst(Nat, z => {Nat.is_le(z, b) == True{} : Bool}, a, Nat.min(a, b), Equal.sym(Nat, Nat.min(a, b), a, N.min_left(a, b, hc)), N.lt_le(a, b, hc))
1295    case False{}:
1296      L.subst(Nat, z => {Nat.is_le(z, b) == True{} : Bool}, b, Nat.min(a, b), Equal.sym(Nat, Nat.min(a, b), b, N.min_right(a, b, hc)), N.le_refl(b))
1297
1298def le_add_rr(+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}:
1299  +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))
1300  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)
1301
1302def comb_top(+K: Nat, +hK: {K == 32n : Nat}, +n: U32, +k: U32, +big: Bool, +hbig: {I.u32_is(NM.Lt{n, k}) == big : Bool}) -> {G.comb_big(~U32, ~I.u32_op, ~I.u32_is, n, k, big) == SG.checked(~U32, ~SG.u32_of, 32n, S.choose(v(n), v(k))) : Result<&2, &2, NM.NumError, U32>}:
1303  match big:
1304    case True{}:
1305      +cz = FA.choose_eq_zero(v(n), v(k), lt_of(n, k, True{}, hbig))
1306      Equal.trans(Result<&2, &2, NM.NumError, U32>, Done{I.u32_op(NM.ZeroOp{})}, SG.checked(~U32, ~SG.u32_of, 32n, 0n), SG.checked(~U32, ~SG.u32_of, 32n, S.choose(v(n), v(k))), Equal.cong(U32, Result<&2, &2, NM.NumError, U32>, t => Done{t}, I.u32_op(NM.ZeroOp{}), of(0n), as_of(I.u32_op(NM.ZeroOp{}), 0n, zero_v())), Equal.cong(Nat, Result<&2, &2, NM.NumError, U32>, t => SG.checked(~U32, ~SG.u32_of, 32n, t), 0n, S.choose(v(n), v(k)), Equal.sym(Nat, S.choose(v(n), v(k)), 0n, cz)))
1307    case False{}:
1308      +hkn = N.not_lt_le(v(n), v(k), lt_of(n, k, False{}, hbig))
1309      +s = I.u32_op(NM.Sub{n, k})
1310      +sn = Nat.sub(v(n), v(k))
1311      +es = Equal.trans(Nat, v(s), Nat.sub(v(n), v(k)), sn, LW.ops_sub(n, k, hkn), {==})
1312      +k0 = Nat.min(v(k), sn)
1313      +kk = G.min(~U32, ~I.u32_op, ~I.u32_is, k, s)
1314      +hk0a = min_le_a(v(k), sn, Nat.is_lt(v(k), sn), {==})
1315      +hk0b = min_le_b(v(k), sn, Nat.is_lt(v(k), sn), {==})
1316      +hkK = L.subst(Nat, z => {Nat.is_lt(z, C.pow2(K)) == True{} : Bool}, v(k), v(k), {==}, U32P.val_lt(1n, {==}, K, hK, k))
1317      +ekk0 = min_c(k, s, I.u32_is(NM.Lt{s, k}), {==})
1318      +ekk1 = Equal.cong(U32, Nat, t => v(t), kk, of(Nat.min(v(k), v(s))), ekk0)
1319      +ekk2 = Equal.cong(Nat, Nat, t => Nat.min(v(k), t), v(s), sn, es)
1320      +hfk = fits32(K, hK, k0, N.le_lt_trans(k0, v(k), C.pow2(K), hk0a, hkK))
1321      +ekk = Equal.trans(Nat, v(kk), v(of(Nat.min(v(k), v(s)))), k0, ekk1, Equal.trans(Nat, v(of(Nat.min(v(k), v(s)))), v(of(k0)), k0, Equal.cong(Nat, Nat, t => v(of(t)), Nat.min(v(k), v(s)), k0, ekk2), LW.vo(k0, hfk)))
1322      +hsum = N.le_trans(Nat.add(k0, k0), Nat.add(v(k), k0), v(n), le_add_rr(k0, v(k), k0, hk0a), L.subst(Nat, z => {Nat.is_le(Nat.add(v(k), k0), z) == True{} : Bool}, Nat.add(v(k), sn), v(n), N.sub_add(v(n), v(k), hkn), N.le_add_left(k0, sn, v(k), hk0b)))
1323      +h2 = L.subst(Nat, z => {Nat.is_le(z, v(n)) == True{} : Bool}, Nat.add(k0, k0), Nat.double(k0), Equal.sym(Nat, Nat.double(k0), Nat.add(k0, k0), NA.double_self(k0)), hsum)
1324      +one = I.u32_op(NM.One{})
1325      +zero = I.u32_op(NM.ZeroOp{})
1326      +c0 = FA.choose_zero_right(v(n))
1327      +hf0 = L.subst(Nat, z => {Nat.is_le(1n+z, 140n) == True{} : Bool}, 32n, K, Equal.sym(Nat, K, 32n, hK), {==})
1328      +hok = L.subst(Nat, z => {C.fits(32n, z) == True{} : Bool}, 1n, S.choose(v(n), 0n), Equal.sym(Nat, S.choose(v(n), 0n), 1n, c0), {==})
1329      +ha = Equal.trans(Nat, v(one), 1n, S.choose(v(n), 0n), one_v(), Equal.sym(Nat, S.choose(v(n), 0n), 1n, c0))
1330      +D = S.choose(v(n), k0)
1331      +sm = combsim(140n, n, zero, kk, one, v(n), 0n, k0, K, True{}, I.u32_is(NM.Lt{zero, kk}), C.fits(32n, D), hK, {==}, zero_v(), ekk, h2, N.zero_le(k0), hf0, hok, ha, ltv(zero, kk, 0n, k0, zero_v(), ekk), {==})
1332      +g = G.comb_go(~U32, ~I.u32_op, ~I.u32_is, 140n, n, zero, kk, (one, True{}), I.u32_is(NM.Lt{zero, kk}))
1333      +em = FA.comb_min(v(n), v(k), hkn, Nat.is_lt(v(k), sn), {==})
1334      Equal.trans(Result<&2, &2, NM.NumError, U32>, G.ok(U32, g), SG.checked(~U32, ~SG.u32_of, 32n, D), SG.checked(~U32, ~SG.u32_of, 32n, S.choose(v(n), v(k))), Equal.trans(Result<&2, &2, NM.NumError, U32>, G.ok(U32, g), G.ok(U32, G.fits(U32, Bool.not(C.fits(32n, D)), of(D))), SG.checked(~U32, ~SG.u32_of, 32n, D), Equal.cong(Maybe<&2, U32>, Result<&2, &2, NM.NumError, U32>, t => G.ok(U32, t), g, G.fits(U32, Bool.not(C.fits(32n, D)), of(D)), sm), okfits(D, C.fits(32n, D))), Equal.cong(Nat, Result<&2, &2, NM.NumError, U32>, t => SG.checked(~U32, ~SG.u32_of, 32n, t), D, S.choose(v(n), v(k)), em))
1335
1336def comb_checked(+n: U32, +k: U32) -> SG.Comb.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, n, k):
1337  Equal.trans(Result<&2, &2, NM.NumError, U32>, G.comb_big(~U32, ~I.u32_op, ~I.u32_is, n, k, I.u32_is(NM.Lt{n, k})), SG.checked(~U32, ~SG.u32_of, 32n, S.choose(v(n), v(k))), SG.checked(~U32, ~SG.u32_of, 32n, M.comb(v(n), v(k))), comb_top(32n, {==}, n, k, I.u32_is(NM.Lt{n, k}), {==}), Equal.cong(Nat, Result<&2, &2, NM.NumError, U32>, t => SG.checked(~U32, ~SG.u32_of, 32n, t), S.choose(v(n), v(k)), M.comb(v(n), v(k)), Equal.sym(Nat, M.comb(v(n), v(k)), S.choose(v(n), v(k)), FA.comb_ok(v(n), v(k)))))