1 import Base 2 import ../../lib/nat.bend as N 3 import ../../lib/logic.bend as L 4 import ../../lib/arith.bend as AR 5 import ../../lib/lemmas/proofs/nat_algebra.bend as A 6 import ../../../src/math/number.bend as NB 7 import ../../../spec/math/number.bend as SN 8 import ../natural/arith.bend as R 9 import ../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 20 def 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)) 30 def 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 41 def 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 46 def 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 52 def 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 62 def 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 72 def 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 80 def 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 87 def 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 99 def 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 102 def 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 106 def 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 113 def 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 120 def 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 128 def 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) 140 def 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 144 def 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 157 def 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 168 def 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 178 def 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 181 def 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 200 def 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), {==}, {==}, {==})