Prime.c_big: 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 112-118 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=112&end_line=118

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/arith.bend as AR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF

# ... and q >= d gives d * d <= q * d <= q * e == n, against n < d * d
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:
  +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)))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=mul_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=true_not_false
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=eq_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_lt_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_irrefl
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend&name=mul_le_r