Prime.at_c: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/number/prime.bend as Prime
Lines 51-60 of bend-collections-laws-math@1.0.0.0/proofs/math/number/prime.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/number/prime.bend&start_line=51&end_line=60

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
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

# a d with lo <= e < lo + k, where nodiv(k, n, lo) holds, does not divide n
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}:
  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)

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_succ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=not_true
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=eq_from_is_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_or_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_succ_le_succ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/number.bend&name=nodiv