proofs/math/typed/u64int.bend

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