def big

bend-collections-laws-math@1.0.0.0 · proofs/math/number/prime.bend:156

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
import bend-collections-laws-math@1.0.0.0/spec/math/number.bend as SN

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))