~/bend-docscommunity

proofs/math/number/prime.bend source

proofs/math/number/prime.bend on the hub · documented module

import Baseimport ../../lib/nat.bend as Nimport ../../lib/logic.bend as Limport ../../lib/arith.bend as ARimport ../../lib/lemmas/proofs/nat_algebra.bend as Aimport ../../../src/math/number.bend as NBimport ../../../spec/math/number.bend as SNimport ../natural/arith.bend as Rimport ../typed/natfuel.bend as NF# Trial division decides primality (Lean 4 Mathlib Nat.Prime: 2 <= n and no# divisor in [2, n); the stopping bound is Nat.minFac_sq_le_self: the least# divisor d of a composite n has d * d <= n). The loop visits d = 2, 3, ...# while d * d <= n and stops at the first divisor; once d * d > n with no# divisor below d, none lies in [d, n) either: a divisor e >= d would give# n == c * e with 2 <= c < d dividing n.# ---- small order facts ----def sub_big(+n: Nat, +d: Nat, +h: {Nat.is_le(n, d) == True{} : Bool}) -> {Nat.sub(n, d) == 0n : Nat}:  match n d:    case 0n _:      R.zsub(d)    case 1n+np 0n:      Empty.absurd({Nat.sub(1n+np, 0n) == 0n : Nat}, L.false_true(h))    case 1n+ +np 1n+ +dp:      sub_big(np, dp, h)# d < n: n - d == 1 + (n - (d + 1))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}:  match n d:    case 0n _:      Empty.absurd({Nat.sub(0n, d) == 1n+Nat.sub(0n, 1n+d) : Nat}, N.lt_zero_absurd(d, h))    case 1n+ +np 0n:      %Equal.sym(Nat, Nat.sub(np, 0n), np, N.sub_zero(np)) : {1n+np == 1n+_ : Nat}      {==}    case 1n+ +np 1n+ +dp:      sub_split(np, dp, h)# 2 <= d: d < d * ddef lt_sq(+dq: Nat) -> {Nat.is_lt(2n+dq, Nat.mul(2n+dq, 2n+dq)) == True{} : Bool}:  +h1 = NF.dbl_le_mul(2n+dq, dq)  +h2 = N.succ_le_lt(2n+dq, Nat.double(2n+dq), N.double_succ_le(2n+dq, {==}))  N.lt_le_trans(2n+dq, Nat.double(2n+dq), Nat.mul(2n+dq, 2n+dq), h2, h1)def le_step(+d: Nat, +e: Nat, +h: {Nat.is_le(d, e) == True{} : Bool}) -> {Nat.is_le(d, 1n+e) == True{} : Bool}:  N.le_trans(d, e, 1n+e, h, N.le_succ(e))# ---- nodiv ----# a d with lo <= e < lo + k, where nodiv(k, n, lo) holds, does not divide ndef 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}:  match c:    case True{}:      %N.eq_from_is_eq(d, e, hc) : {Nat.is_eq(Nat.mod(n, _), 0n) == False{} : Bool}      L.not_true(Nat.is_eq(Nat.mod(n, d), 0n), h1)    case False{}:      +hlt = N.lt_or_eq(d, e, hlo, hc)      +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)      ih(e, N.lt_succ_le_succ(d, e, hlt), hh)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}:  match k:    case 0n:      +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)      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)))    case 1n+ +p:      +h1 = L.and_left(Bool.not(Nat.is_eq(Nat.mod(n, d), 0n)), SN.nodiv(p, n, 1n+d), h)      +h2 = L.and_right(Bool.not(Nat.is_eq(Nat.mod(n, d), 0n)), SN.nodiv(p, n, 1n+d), h)      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))def and_true(+b: Bool) -> {Bool.and(b, True{}) == b : Bool}:  match b:    case False{}:      {==}    case True{}:      {==}# nodiv(1 + k, n, d) adds the test of d + kdef and_assoc(+x: Bool, +y: Bool, +z: Bool) -> {Bool.and(x, Bool.and(y, z)) == Bool.and(Bool.and(x, y), z) : Bool}:  match x:    case True{}:      {==}    case False{}:      {==}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}:  match k:    case 0n:      %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}      and_true(Bool.not(Nat.is_eq(Nat.mod(n, d), 0n)))    case 1n+ +m:      %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}      %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}      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)))# ---- no divisor above sqrt(n) without one below ----def mul0(+x: Nat) -> {Nat.mul(0n, x) == 0n : Nat}:  Equal.trans(Nat, Nat.mul(0n, x), Nat.mul(x, 0n), 0n, A.mul_comm(0n, x), A.mul_zero(x))def mul1(+x: Nat) -> {Nat.mul(1n, x) == x : Nat}:  Equal.trans(Nat, Nat.mul(1n, x), Nat.mul(x, 1n), x, A.mul_comm(1n, x), A.mul_one(x))# n == q e with q >= 2 and q < d would divide n, which nodiv(dq, n, 2) rules outdef 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:  +hf = nodiv_at(dq, n, 2n, 2n+qq, hs, N.zero_le(qq), hq)  +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, {==}))  +ht = Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), Nat.mod(n, 2n+qq), 0n, hm)  L.true_not_false(Nat.is_eq(Nat.mod(n, 2n+qq), 0n), ht, hf)# ... and q >= d gives d * d <= q * d <= q * e == n, against n < d * ddef 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:  +h1 = AR.mul_le(2n+dq, q, 2n+dq, hq)  +h2 = NF.mul_le_r(q, 2n+dq, 2n+eq, hde)  +h3 = N.eq_le(Nat.mul(q, 2n+eq), n, Equal.sym(Nat, n, Nat.mul(q, 2n+eq), hn))  +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))  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)))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:  match c:    case True{}:      c_small(n, dq, eq, qq, hn, hs, hc)    case False{}:      c_big(n, dq, eq, 2n+qq, hn, hdd, hde, N.not_lt_le(2n+qq, 2n+dq, hc))# e divides n with d <= e < n, d * d > n and no divisor in [2, d): impossibledef 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:  match q:    case 0n:      +hz = Equal.trans(Nat, n, Nat.mul(0n, 2n+eq), 0n, hn, mul0(2n+eq))      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))    case 1n:      +he = Equal.trans(Nat, n, Nat.mul(1n, 2n+eq), 2n+eq, hn, mul1(2n+eq))      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))    case 2n+ +qq:      c_two(n, dq, eq, qq, hn, hdd, hs, hde, Nat.is_lt(2n+qq, 2n+dq), {==})# e < e + (1 + p)def lt_add1(+e: Nat, +p: Nat) -> {Nat.is_lt(e, Nat.add(e, 1n+p)) == True{} : Bool}:  %Equal.sym(Nat, Nat.add(e, 1n+p), 1n+Nat.add(e, p), A.add_succ(e, p)) : {Nat.is_lt(e, _) == True{} : Bool}  N.le_lt_succ(e, Nat.add(e, p), N.le_add_right(e, p))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}:  match c:    case False{}:      %Equal.sym(Bool, Nat.is_eq(Nat.mod(n, 2n+eq), 0n), False{}, hc) : {Bool.not(_) == True{} : Bool}      {==}    case True{}:      +hm = N.eq_from_is_eq(Nat.mod(n, 2n+eq), 0n, hc)      +hn0 = R.dm_eq(1n+eq, n)      +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))))      +hen = N.lt_le_trans(2n+eq, Nat.add(2n+eq, 1n+p), n, lt_add1(2n+eq, p), hek)      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))# every e in [2 + eq, 2 + eq + k) with d <= e, e + k <= n: none divides ndef 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}:  match k:    case 0n:      {==}    case 1n+ +p:      +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)      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))# ---- the loop ----# the stop at d * d > n: nothing in [d, n) divides ndef 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}:  match c:    case True{}:      +hk = N.eq_le(Nat.add(2n+dq, Nat.sub(n, 2n+dq)), n, N.sub_add(n, 2n+dq, hc))      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))    case False{}:      %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}      {==}# d * d <= n: d < ndef 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}:  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))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}:  match f done dv:    case 0n _ _:      +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))      %Equal.sym(Nat, Nat.sub(n, 2n+dq), 0n, sub_big(n, 2n+dq, hle)) : {True{} == SN.nodiv(_, n, 2n+dq) : Bool}      {==}    case 1n+ +g True{} _:      stop(n, dq, hdone, hs, Nat.is_le(2n+dq, n), {==})    case 1n+ +g False{} True{}:      %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}      %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}      {==}    case 1n+ +g False{} False{}:      %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}      %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}      +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)))      +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)      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)def is_prime_value(+n: Nat) -> SN.IsPrime.value(n):  match n:    case 0n:      {==}    case 1n:      {==}    case 2n+ +p:      %N.sub_zero(p) : {NB.is_prime(2n+p) == SN.nodiv(_, 2n+p, 2n) : Bool}      loop(2n+p, 2n+p, 0n, Nat.is_lt(2n+p, 4n), {==}, Nat.is_eq(Nat.mod(2n+p, 2n), 0n), {==}, {==}, {==})