proofs/math/number/prime.bend

bend-collections-laws-math@1.0.0.0 · 208 lines · 22 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
3import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
4import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as AR
5import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
6import bend-collections-laws-math@1.0.0.0/src/math/number.bend as NB
7import bend-collections-laws-math@1.0.0.0/spec/math/number.bend as SN
8import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as R
9import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF
10
11# Trial division decides primality (Lean 4 Mathlib Nat.Prime: 2 <= n and no
12# divisor in [2, n); the stopping bound is Nat.minFac_sq_le_self: the least
13# divisor d of a composite n has d * d <= n). The loop visits d = 2, 3, ...
14# while d * d <= n and stops at the first divisor; once d * d > n with no
15# divisor below d, none lies in [d, n) either: a divisor e >= d would give
16# n == c * e with 2 <= c < d dividing n.
17
18# ---- small order facts ----
19
20def sub_big(+n: Nat, +d: Nat, +h: {Nat.is_le(n, d) == True{} : Bool}) -> {Nat.sub(n, d) == 0n : Nat}:
21  match n d:
22    case 0n _:
23      R.zsub(d)
24    case 1n+np 0n:
25      Empty.absurd({Nat.sub(1n+np, 0n) == 0n : Nat}, L.false_true(h))
26    case 1n+ +np 1n+ +dp:
27      sub_big(np, dp, h)
28
29# d < n: n - d == 1 + (n - (d + 1))
30def sub_split(+n: Nat, +d: Nat, +h: {Nat.is_lt(d, n) == True{} : Bool}) -> {Nat.sub(n, d) == 1n+Nat.sub(n, 1n+d) : Nat}:
31  match n d:
32    case 0n _:
33      Empty.absurd({Nat.sub(0n, d) == 1n+Nat.sub(0n, 1n+d) : Nat}, N.lt_zero_absurd(d, h))
34    case 1n+ +np 0n:
35      %Equal.sym(Nat, Nat.sub(np, 0n), np, N.sub_zero(np)) : {1n+np == 1n+_ : Nat}
36      {==}
37    case 1n+ +np 1n+ +dp:
38      sub_split(np, dp, h)
39
40# 2 <= d: d < d * d
41def lt_sq(+dq: Nat) -> {Nat.is_lt(2n+dq, Nat.mul(2n+dq, 2n+dq)) == True{} : Bool}:
42  +h1 = NF.dbl_le_mul(2n+dq, dq)
43  +h2 = N.succ_le_lt(2n+dq, Nat.double(2n+dq), N.double_succ_le(2n+dq, {==}))
44  N.lt_le_trans(2n+dq, Nat.double(2n+dq), Nat.mul(2n+dq, 2n+dq), h2, h1)
45
46def le_step(+d: Nat, +e: Nat, +h: {Nat.is_le(d, e) == True{} : Bool}) -> {Nat.is_le(d, 1n+e) == True{} : Bool}:
47  N.le_trans(d, e, 1n+e, h, N.le_succ(e))
48
49# ---- nodiv ----
50
51# a d with lo <= e < lo + k, where nodiv(k, n, lo) holds, does not divide n
52def at_c(p: Nat, +n: Nat, +d: Nat, +e: Nat, +h1: {Bool.not(Nat.is_eq(Nat.mod(n, d), 0n)) == True{} : Bool}, +h2: {SN.nodiv(p, n, 1n+d) == True{} : Bool}, +hlo: {Nat.is_le(d, e) == True{} : Bool}, +hhi: {Nat.is_lt(e, Nat.add(d, 1n+p)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(d, e) == c : Bool}, ih: @+e2: Nat -> @+hl: {Nat.is_le(1n+d, e2) == True{} : Bool} -> @+hh: {Nat.is_lt(e2, Nat.add(1n+d, p)) == True{} : Bool} -> {Nat.is_eq(Nat.mod(n, e2), 0n) == False{} : Bool}) -> {Nat.is_eq(Nat.mod(n, e), 0n) == False{} : Bool}:
53  match c:
54    case True{}:
55      %N.eq_from_is_eq(d, e, hc) : {Nat.is_eq(Nat.mod(n, _), 0n) == False{} : Bool}
56      L.not_true(Nat.is_eq(Nat.mod(n, d), 0n), h1)
57    case False{}:
58      +hlt = N.lt_or_eq(d, e, hlo, hc)
59      +hh = Equal.trans(Bool, Nat.is_lt(e, 1n+Nat.add(d, p)), Nat.is_lt(e, Nat.add(d, 1n+p)), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(e, t), 1n+Nat.add(d, p), Nat.add(d, 1n+p), Equal.sym(Nat, Nat.add(d, 1n+p), 1n+Nat.add(d, p), A.add_succ(d, p))), hhi)
60      ih(e, N.lt_succ_le_succ(d, e, hlt), hh)
61
62def nodiv_at(k: Nat, +n: Nat, +d: Nat, +e: Nat, +h: {SN.nodiv(k, n, d) == True{} : Bool}, +hlo: {Nat.is_le(d, e) == True{} : Bool}, +hhi: {Nat.is_lt(e, Nat.add(d, k)) == True{} : Bool}) -> {Nat.is_eq(Nat.mod(n, e), 0n) == False{} : Bool}:
63  match k:
64    case 0n:
65      +hh = Equal.trans(Bool, Nat.is_lt(e, d), Nat.is_lt(e, Nat.add(d, 0n)), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(e, t), d, Nat.add(d, 0n), Equal.sym(Nat, Nat.add(d, 0n), d, A.add_zero(d))), hhi)
66      Empty.absurd({Nat.is_eq(Nat.mod(n, e), 0n) == False{} : Bool}, L.true_not_false(Nat.is_lt(d, d), N.le_lt_trans(d, e, d, hlo, hh), N.lt_irrefl(d)))
67    case 1n+ +p:
68      +h1 = L.and_left(Bool.not(Nat.is_eq(Nat.mod(n, d), 0n)), SN.nodiv(p, n, 1n+d), h)
69      +h2 = L.and_right(Bool.not(Nat.is_eq(Nat.mod(n, d), 0n)), SN.nodiv(p, n, 1n+d), h)
70      at_c(p, n, d, e, h1, h2, hlo, hhi, Nat.is_eq(d, e), {==}, e2 => hl => hh => nodiv_at(p, n, 1n+d, e2, h2, hl, hh))
71
72def and_true(+b: Bool) -> {Bool.and(b, True{}) == b : Bool}:
73  match b:
74    case False{}:
75      {==}
76    case True{}:
77      {==}
78
79# nodiv(1 + k, n, d) adds the test of d + k
80def and_assoc(+x: Bool, +y: Bool, +z: Bool) -> {Bool.and(x, Bool.and(y, z)) == Bool.and(Bool.and(x, y), z) : Bool}:
81  match x:
82    case True{}:
83      {==}
84    case False{}:
85      {==}
86
87def snoc(k: Nat, +n: Nat, +d: Nat) -> {SN.nodiv(1n+k, n, d) == Bool.and(SN.nodiv(k, n, d), Bool.not(Nat.is_eq(Nat.mod(n, Nat.add(d, k)), 0n))) : Bool}:
88  match k:
89    case 0n:
90      %Equal.sym(Nat, Nat.add(d, 0n), d, A.add_zero(d)) : {SN.nodiv(1n, n, d) == Bool.and(True{}, Bool.not(Nat.is_eq(Nat.mod(n, _), 0n))) : Bool}
91      and_true(Bool.not(Nat.is_eq(Nat.mod(n, d), 0n)))
92    case 1n+ +m:
93      %Equal.sym(Nat, Nat.add(d, 1n+m), 1n+Nat.add(d, m), A.add_succ(d, m)) : {SN.nodiv(2n+m, n, d) == Bool.and(SN.nodiv(1n+m, n, d), Bool.not(Nat.is_eq(Nat.mod(n, _), 0n))) : Bool}
94      %Equal.sym(Bool, SN.nodiv(1n+m, n, 1n+d), Bool.and(SN.nodiv(m, n, 1n+d), Bool.not(Nat.is_eq(Nat.mod(n, Nat.add(1n+d, m)), 0n))), snoc(m, n, 1n+d)) : {Bool.and(Bool.not(Nat.is_eq(Nat.mod(n, d), 0n)), _) == Bool.and(SN.nodiv(1n+m, n, d), Bool.not(Nat.is_eq(Nat.mod(n, 1n+Nat.add(d, m)), 0n))) : Bool}
95      and_assoc(Bool.not(Nat.is_eq(Nat.mod(n, d), 0n)), SN.nodiv(m, n, 1n+d), Bool.not(Nat.is_eq(Nat.mod(n, 1n+Nat.add(d, m)), 0n)))
96
97# ---- no divisor above sqrt(n) without one below ----
98
99def mul0(+x: Nat) -> {Nat.mul(0n, x) == 0n : Nat}:
100  Equal.trans(Nat, Nat.mul(0n, x), Nat.mul(x, 0n), 0n, A.mul_comm(0n, x), A.mul_zero(x))
101
102def mul1(+x: Nat) -> {Nat.mul(1n, x) == x : Nat}:
103  Equal.trans(Nat, Nat.mul(1n, x), Nat.mul(x, 1n), x, A.mul_comm(1n, x), A.mul_one(x))
104
105# n == q e with q >= 2 and q < d would divide n, which nodiv(dq, n, 2) rules out
106def c_small(+n: Nat, +dq: Nat, +eq: Nat, +qq: Nat, +hn: {n == Nat.mul(2n+qq, 2n+eq) : Nat}, +hs: {SN.nodiv(dq, n, 2n) == True{} : Bool}, +hq: {Nat.is_lt(2n+qq, 2n+dq) == True{} : Bool}) -> Empty:
107  +hf = nodiv_at(dq, n, 2n, 2n+qq, hs, N.zero_le(qq), hq)
108  +hm = Equal.trans(Nat, Nat.mod(n, 2n+qq), Nat.mod(Nat.add(Nat.mul(2n+eq, 2n+qq), 0n), 2n+qq), 0n, Equal.cong(Nat, Nat, t => Nat.mod(t, 2n+qq), n, Nat.add(Nat.mul(2n+eq, 2n+qq), 0n), Equal.trans(Nat, n, Nat.mul(2n+qq, 2n+eq), Nat.add(Nat.mul(2n+eq, 2n+qq), 0n), hn, Equal.trans(Nat, Nat.mul(2n+qq, 2n+eq), Nat.mul(2n+eq, 2n+qq), Nat.add(Nat.mul(2n+eq, 2n+qq), 0n), A.mul_comm(2n+qq, 2n+eq), Equal.sym(Nat, Nat.add(Nat.mul(2n+eq, 2n+qq), 0n), Nat.mul(2n+eq, 2n+qq), A.add_zero(Nat.mul(2n+eq, 2n+qq)))))), R.mod_of(2n+eq, 1n+qq, 0n, {==}))
109  +ht = Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), Nat.mod(n, 2n+qq), 0n, hm)
110  L.true_not_false(Nat.is_eq(Nat.mod(n, 2n+qq), 0n), ht, hf)
111
112# ... and q >= d gives d * d <= q * d <= q * e == n, against n < d * d
113def c_big(+n: Nat, +dq: Nat, +eq: Nat, +q: Nat, +hn: {n == Nat.mul(q, 2n+eq) : Nat}, +hdd: {Nat.is_lt(n, Nat.mul(2n+dq, 2n+dq)) == True{} : Bool}, +hde: {Nat.is_le(2n+dq, 2n+eq) == True{} : Bool}, +hq: {Nat.is_le(2n+dq, q) == True{} : Bool}) -> Empty:
114  +h1 = AR.mul_le(2n+dq, q, 2n+dq, hq)
115  +h2 = NF.mul_le_r(q, 2n+dq, 2n+eq, hde)
116  +h3 = N.eq_le(Nat.mul(q, 2n+eq), n, Equal.sym(Nat, n, Nat.mul(q, 2n+eq), hn))
117  +h4 = N.le_trans(Nat.mul(2n+dq, 2n+dq), Nat.mul(q, 2n+dq), n, h1, N.le_trans(Nat.mul(q, 2n+dq), Nat.mul(q, 2n+eq), n, h2, h3))
118  L.true_not_false(Nat.is_lt(Nat.mul(2n+dq, 2n+dq), Nat.mul(2n+dq, 2n+dq)), N.le_lt_trans(Nat.mul(2n+dq, 2n+dq), n, Nat.mul(2n+dq, 2n+dq), h4, hdd), N.lt_irrefl(Nat.mul(2n+dq, 2n+dq)))
119
120def c_two(+n: Nat, +dq: Nat, +eq: Nat, +qq: Nat, +hn: {n == Nat.mul(2n+qq, 2n+eq) : Nat}, +hdd: {Nat.is_lt(n, Nat.mul(2n+dq, 2n+dq)) == True{} : Bool}, +hs: {SN.nodiv(dq, n, 2n) == True{} : Bool}, +hde: {Nat.is_le(2n+dq, 2n+eq) == True{} : Bool}, +c: Bool, +hc: {Nat.is_lt(2n+qq, 2n+dq) == c : Bool}) -> Empty:
121  match c:
122    case True{}:
123      c_small(n, dq, eq, qq, hn, hs, hc)
124    case False{}:
125      c_big(n, dq, eq, 2n+qq, hn, hdd, hde, N.not_lt_le(2n+qq, 2n+dq, hc))
126
127# e divides n with d <= e < n, d * d > n and no divisor in [2, d): impossible
128def contra(+n: Nat, +dq: Nat, +eq: Nat, +q: Nat, +hn: {n == Nat.mul(q, 2n+eq) : Nat}, +hen: {Nat.is_lt(2n+eq, n) == True{} : Bool}, +hdd: {Nat.is_lt(n, Nat.mul(2n+dq, 2n+dq)) == True{} : Bool}, +hs: {SN.nodiv(dq, n, 2n) == True{} : Bool}, +hde: {Nat.is_le(2n+dq, 2n+eq) == True{} : Bool}) -> Empty:
129  match q:
130    case 0n:
131      +hz = Equal.trans(Nat, n, Nat.mul(0n, 2n+eq), 0n, hn, mul0(2n+eq))
132      N.lt_zero_absurd(2n+eq, Equal.trans(Bool, Nat.is_lt(2n+eq, 0n), Nat.is_lt(2n+eq, n), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(2n+eq, t), 0n, n, Equal.sym(Nat, n, 0n, hz)), hen))
133    case 1n:
134      +he = Equal.trans(Nat, n, Nat.mul(1n, 2n+eq), 2n+eq, hn, mul1(2n+eq))
135      L.true_not_false(Nat.is_lt(2n+eq, 2n+eq), Equal.trans(Bool, Nat.is_lt(2n+eq, 2n+eq), Nat.is_lt(2n+eq, n), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(2n+eq, t), 2n+eq, n, Equal.sym(Nat, n, 2n+eq, he)), hen), N.lt_irrefl(2n+eq))
136    case 2n+ +qq:
137      c_two(n, dq, eq, qq, hn, hdd, hs, hde, Nat.is_lt(2n+qq, 2n+dq), {==})
138
139# e < e + (1 + p)
140def lt_add1(+e: Nat, +p: Nat) -> {Nat.is_lt(e, Nat.add(e, 1n+p)) == True{} : Bool}:
141  %Equal.sym(Nat, Nat.add(e, 1n+p), 1n+Nat.add(e, p), A.add_succ(e, p)) : {Nat.is_lt(e, _) == True{} : Bool}
142  N.le_lt_succ(e, Nat.add(e, p), N.le_add_right(e, p))
143
144def head_c(+n: Nat, +dq: Nat, +eq: Nat, +p: Nat, +hdd: {Nat.is_lt(n, Nat.mul(2n+dq, 2n+dq)) == True{} : Bool}, +hs: {SN.nodiv(dq, n, 2n) == True{} : Bool}, +hde: {Nat.is_le(2n+dq, 2n+eq) == True{} : Bool}, +hek: {Nat.is_le(Nat.add(2n+eq, 1n+p), n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(Nat.mod(n, 2n+eq), 0n) == c : Bool}) -> {Bool.not(Nat.is_eq(Nat.mod(n, 2n+eq), 0n)) == True{} : Bool}:
145  match c:
146    case False{}:
147      %Equal.sym(Bool, Nat.is_eq(Nat.mod(n, 2n+eq), 0n), False{}, hc) : {Bool.not(_) == True{} : Bool}
148      {==}
149    case True{}:
150      +hm = N.eq_from_is_eq(Nat.mod(n, 2n+eq), 0n, hc)
151      +hn0 = R.dm_eq(1n+eq, n)
152      +hn1 = Equal.trans(Nat, n, Nat.add(Nat.mul(Nat.div(n, 2n+eq), 2n+eq), Nat.mod(n, 2n+eq)), Nat.mul(Nat.div(n, 2n+eq), 2n+eq), hn0, Equal.trans(Nat, Nat.add(Nat.mul(Nat.div(n, 2n+eq), 2n+eq), Nat.mod(n, 2n+eq)), Nat.add(Nat.mul(Nat.div(n, 2n+eq), 2n+eq), 0n), Nat.mul(Nat.div(n, 2n+eq), 2n+eq), Equal.cong(Nat, Nat, t => Nat.add(Nat.mul(Nat.div(n, 2n+eq), 2n+eq), t), Nat.mod(n, 2n+eq), 0n, hm), A.add_zero(Nat.mul(Nat.div(n, 2n+eq), 2n+eq))))
153      +hen = N.lt_le_trans(2n+eq, Nat.add(2n+eq, 1n+p), n, lt_add1(2n+eq, p), hek)
154      Empty.absurd({Bool.not(Nat.is_eq(Nat.mod(n, 2n+eq), 0n)) == True{} : Bool}, contra(n, dq, eq, Nat.div(n, 2n+eq), hn1, hen, hdd, hs, hde))
155
156# every e in [2 + eq, 2 + eq + k) with d <= e, e + k <= n: none divides n
157def big(k: Nat, +n: Nat, +dq: Nat, +eq: Nat, +hdd: {Nat.is_lt(n, Nat.mul(2n+dq, 2n+dq)) == True{} : Bool}, +hs: {SN.nodiv(dq, n, 2n) == True{} : Bool}, +hde: {Nat.is_le(2n+dq, 2n+eq) == True{} : Bool}, +hek: {Nat.is_le(Nat.add(2n+eq, k), n) == True{} : Bool}) -> {SN.nodiv(k, n, 2n+eq) == True{} : Bool}:
158  match k:
159    case 0n:
160      {==}
161    case 1n+ +p:
162      +hk2 = Equal.trans(Bool, Nat.is_le(Nat.add(3n+eq, p), n), Nat.is_le(Nat.add(2n+eq, 1n+p), n), True{}, Equal.cong(Nat, Bool, t => Nat.is_le(t, n), Nat.add(3n+eq, p), Nat.add(2n+eq, 1n+p), Equal.sym(Nat, Nat.add(2n+eq, 1n+p), 1n+Nat.add(2n+eq, p), A.add_succ(2n+eq, p))), hek)
163      L.and_intro(Bool.not(Nat.is_eq(Nat.mod(n, 2n+eq), 0n)), SN.nodiv(p, n, 3n+eq), head_c(n, dq, eq, p, hdd, hs, hde, hek, Nat.is_eq(Nat.mod(n, 2n+eq), 0n), {==}), big(p, n, dq, 1n+eq, hdd, hs, le_step(2n+dq, 2n+eq, hde), hk2))
164
165# ---- the loop ----
166
167# the stop at d * d > n: nothing in [d, n) divides n
168def stop(+n: Nat, +dq: Nat, +hdd: {Nat.is_lt(n, Nat.mul(2n+dq, 2n+dq)) == True{} : Bool}, +hs: {SN.nodiv(dq, n, 2n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_le(2n+dq, n) == c : Bool}) -> {True{} == SN.nodiv(Nat.sub(n, 2n+dq), n, 2n+dq) : Bool}:
169  match c:
170    case True{}:
171      +hk = N.eq_le(Nat.add(2n+dq, Nat.sub(n, 2n+dq)), n, N.sub_add(n, 2n+dq, hc))
172      Equal.sym(Bool, SN.nodiv(Nat.sub(n, 2n+dq), n, 2n+dq), True{}, big(Nat.sub(n, 2n+dq), n, dq, dq, hdd, hs, N.le_refl(2n+dq), hk))
173    case False{}:
174      %Equal.sym(Nat, Nat.sub(n, 2n+dq), 0n, sub_big(n, 2n+dq, N.lt_le(n, 2n+dq, N.not_le_lt(2n+dq, n, hc)))) : {True{} == SN.nodiv(_, n, 2n+dq) : Bool}
175      {==}
176
177# d * d <= n: d < n
178def below(+n: Nat, +dq: Nat, +hdd: {Nat.is_lt(n, Nat.mul(2n+dq, 2n+dq)) == False{} : Bool}) -> {Nat.is_lt(2n+dq, n) == True{} : Bool}:
179  N.lt_le_trans(2n+dq, Nat.mul(2n+dq, 2n+dq), n, lt_sq(dq), N.not_lt_le(n, Nat.mul(2n+dq, 2n+dq), hdd))
180
181def loop(+f: Nat, +n: Nat, +dq: Nat, +done: Bool, +hdone: {Nat.is_lt(n, Nat.mul(2n+dq, 2n+dq)) == done : Bool}, +dv: Bool, +hdv: {Nat.is_eq(Nat.mod(n, 2n+dq), 0n) == dv : Bool}, +hs: {SN.nodiv(dq, n, 2n) == True{} : Bool}, +hf: {Nat.add(f, 2n+dq) == Nat.add(n, 2n) : Nat}) -> {NB.prime_go(f, n, 2n+dq, done, dv) == SN.nodiv(Nat.sub(n, 2n+dq), n, 2n+dq) : Bool}:
182  match f done dv:
183    case 0n _ _:
184      +hle = Equal.trans(Bool, Nat.is_le(n, 2n+dq), Nat.is_le(n, Nat.add(n, 2n)), True{}, Equal.cong(Nat, Bool, t => Nat.is_le(n, t), 2n+dq, Nat.add(n, 2n), hf), N.le_add_right(n, 2n))
185      %Equal.sym(Nat, Nat.sub(n, 2n+dq), 0n, sub_big(n, 2n+dq, hle)) : {True{} == SN.nodiv(_, n, 2n+dq) : Bool}
186      {==}
187    case 1n+ +g True{} _:
188      stop(n, dq, hdone, hs, Nat.is_le(2n+dq, n), {==})
189    case 1n+ +g False{} True{}:
190      %Equal.sym(Nat, Nat.sub(n, 2n+dq), 1n+Nat.sub(n, 3n+dq), sub_split(n, 2n+dq, below(n, dq, hdone))) : {False{} == SN.nodiv(_, n, 2n+dq) : Bool}
191      %Equal.sym(Bool, Nat.is_eq(Nat.mod(n, 2n+dq), 0n), True{}, hdv) : {False{} == Bool.and(Bool.not(_), SN.nodiv(Nat.sub(n, 3n+dq), n, 3n+dq)) : Bool}
192      {==}
193    case 1n+ +g False{} False{}:
194      %Equal.sym(Nat, Nat.sub(n, 2n+dq), 1n+Nat.sub(n, 3n+dq), sub_split(n, 2n+dq, below(n, dq, hdone))) : {NB.prime_go(g, n, 3n+dq, Nat.is_lt(n, Nat.mul(3n+dq, 3n+dq)), Nat.is_eq(Nat.mod(n, 3n+dq), 0n)) == SN.nodiv(_, n, 2n+dq) : Bool}
195      %Equal.sym(Bool, Nat.is_eq(Nat.mod(n, 2n+dq), 0n), False{}, hdv) : {NB.prime_go(g, n, 3n+dq, Nat.is_lt(n, Nat.mul(3n+dq, 3n+dq)), Nat.is_eq(Nat.mod(n, 3n+dq), 0n)) == Bool.and(Bool.not(_), SN.nodiv(Nat.sub(n, 3n+dq), n, 3n+dq)) : Bool}
196      +hs2 = Equal.trans(Bool, SN.nodiv(1n+dq, n, 2n), Bool.and(SN.nodiv(dq, n, 2n), Bool.not(Nat.is_eq(Nat.mod(n, Nat.add(2n, dq)), 0n))), True{}, snoc(dq, n, 2n), L.and_intro(SN.nodiv(dq, n, 2n), Bool.not(Nat.is_eq(Nat.mod(n, 2n+dq), 0n)), hs, L.not_false(Nat.is_eq(Nat.mod(n, 2n+dq), 0n), hdv)))
197      +hf2 = Equal.trans(Nat, Nat.add(g, 3n+dq), 1n+Nat.add(g, 2n+dq), Nat.add(n, 2n), A.add_succ(g, 2n+dq), hf)
198      loop(g, n, 1n+dq, Nat.is_lt(n, Nat.mul(3n+dq, 3n+dq)), {==}, Nat.is_eq(Nat.mod(n, 3n+dq), 0n), {==}, hs2, hf2)
199
200def is_prime_value(+n: Nat) -> SN.IsPrime.value(n):
201  match n:
202    case 0n:
203      {==}
204    case 1n:
205      {==}
206    case 2n+ +p:
207      %N.sub_zero(p) : {NB.is_prime(2n+p) == SN.nodiv(_, 2n+p, 2n) : Bool}
208      loop(2n+p, 2n+p, 0n, Nat.is_lt(2n+p, 4n), {==}, Nat.is_eq(Nat.mod(2n+p, 2n), 0n), {==}, {==}, {==})