import Base
import ./mathlib.bend as M
import ./nat.bend as N
import ./primes.bend as P

# ===========================================================================
# euclid.bend -- THERE IS NO LARGEST PRIME, checked.
#
# The theorem at the bottom of the file reads
#
#   for every n there is a p with  n <= p  and  p is prime
#
# and it is stated in the vocabulary of mathlib.bend, the tiny arithmetic
# library the website's math card runs: `M.nat_le` is the Bool comparison
# and `M.is_prime` is Bool trial division -- p is prime when 2 <= p and no
# d with 2 <= d <= p-1 divides it, divisibility being "the remainder of
# repeated subtraction is zero".
#
# THE ARGUMENT, in plain words.
#
#   Let N = n! + 1. It is at least 2, so it has divisors above 1; let p be
#   the SMALLEST of them. Then
#
#     * p is prime, because a divisor of p is a divisor of N, and p was
#       the smallest one above 1: nothing between 2 and p-1 divides p.
#     * p > n, because every d between 2 and n divides n!, and no such d
#       can also divide n! + 1 -- it would have to divide 1.
#
#   So for every n there is a prime at least as large as n: no prime is
#   the largest.
#
# THE PROOF, in the shape the checker wants. Three layers.
#
#   1. Reflection (this file, first half). mathlib decides things with
#      Bools; the argument needs propositions. `M.nat_le`, `M.nat_eq` and
#      `M.msub` are reflected in both directions, and then the interesting
#      one: `M.mod` really is the remainder. mathlib computes it by
#      repeated subtraction under a fuel, so `mgo_lt` and `mgo_eq` prove,
#      by induction on that fuel, that the answer is below the divisor and
#      that quotient*divisor + answer is the input. Those two
#      turn `M.divides(d, x) == True{}` into "some q has q*d = x" and back
#      (`divides_elim`, `divides_intro`).
#
#   2. Structure (../../lib/primes.bend). Divisibility as an existential,
#      its transitivity, the factorial, "every 1 <= d <= n divides n!",
#      and "a divisor of 2 or more never divides two consecutive numbers".
#
#   3. The scan (this file, second half). `scan` walks d = 2, 3, 4, ...
#      through N carrying the invariant `M.has_divisor(N, d-1) == False{}`
#      -- which is literally mathlib's own trial division, so when the
#      scan stops at the first divisor p it hands back exactly the Bool
#      fact that nothing below p divides N. `least_is_prime` turns that
#      into `M.has_divisor(p, p-1) == False{}`, i.e. `M.is_prime(p)`, and
#      `no_largest_prime` puts p above n.
#
# Nothing here is a decision procedure run on a literal: every proof is an
# induction over a variable, so the checker never builds a large Nat.
# ===========================================================================

# ---------------------------------------------------------------------
# 1a. mathlib's Bool tests, reflected into lib/nat.bend's propositions
# ---------------------------------------------------------------------

# nat_eq says True exactly when the two numbers are equal ...
def eq_of_nat_eq(a: Nat, b: Nat, e: {M.nat_eq(a, b) == True{} : Bool}) -> {a == b : Nat}:
  match a b:
    case 0n 0n:
      {==}
    case 0n 1n+q:
      Empty.absurd({0n == 1n+q : Nat}, N.Bool.false_ne_true(e))
    case 1n+p 0n:
      Empty.absurd({1n+p == 0n : Nat}, N.Bool.false_ne_true(e))
    case 1n+p 1n+q:
      Equal.cong(Nat, Nat, x => 1n+x, p, q, eq_of_nat_eq(p, q, e))

# ... and it says True whenever they are.
def nat_eq_of_eq(a: Nat, b: Nat, e: {a == b : Nat}) -> {M.nat_eq(a, b) == True{} : Bool}:
  match a b:
    case 0n 0n:
      {==}
    case 0n 1n+q:
      Empty.absurd({M.nat_eq(0n, 1n+q) == True{} : Bool}, N.Nat.zero_neq_succ(q, e))
    case 1n+p 0n:
      Empty.absurd({M.nat_eq(1n+p, 0n) == True{} : Bool}, N.Nat.succ_neq_zero(p, e))
    case 1n+p 1n+q:
      nat_eq_of_eq(p, q, N.Nat.succ_inj(p, q, e))

# nat_le is Nat.Le, in both directions, and its False answer is a strict >
def le_of_nat_le(a: Nat, b: Nat, e: {M.nat_le(a, b) == True{} : Bool}) -> N.Nat.Le(a, b):
  match a b:
    case 0n 0n:
      Unit{}
    case 0n 1n+q:
      Unit{}
    case 1n+p 0n:
      Empty.absurd(N.Nat.Le(1n+p, 0n), N.Bool.false_ne_true(e))
    case 1n+p 1n+q:
      le_of_nat_le(p, q, e)

def nat_le_of_le(a: Nat, b: Nat, h: N.Nat.Le(a, b)) -> {M.nat_le(a, b) == True{} : Bool}:
  match a b:
    case 0n 0n:
      {==}
    case 0n 1n+q:
      {==}
    case 1n+p 0n:
      match h:
    case 1n+p 1n+q:
      nat_le_of_le(p, q, h)

def lt_of_nat_le_false(a: Nat, b: Nat, e: {M.nat_le(a, b) == False{} : Bool}) -> N.Nat.Le(1n+b, a):
  match a b:
    case 0n 0n:
      Empty.absurd(N.Nat.Le(1n, 0n), N.Bool.true_ne_false(e))
    case 0n 1n+q:
      Empty.absurd(N.Nat.Le(2n+q, 0n), N.Bool.true_ne_false(e))
    case 1n+p 0n:
      Unit{}
    case 1n+p 1n+q:
      lt_of_nat_le_false(p, q, e)

# mathlib's truncated subtraction really subtracts, when it can
def msub_add(b: Nat, a: Nat, h: N.Nat.Le(b, a)) -> {Nat.add(b, M.msub(a, b)) == a : Nat}:
  match b a:
    case 0n 0n:
      {==}
    case 0n 1n+p:
      {==}
    case 1n+q 0n:
      match h:
    case 1n+q 1n+p:
      Equal.cong(Nat, Nat, x => 1n+x, Nat.add(q, M.msub(p, q)), p, msub_add(q, p, h))

# subtracting a positive amount strictly shrinks: this is what makes the
# fuel of `mod` run down
def msub_lt(+x: Nat, +dp: Nat, h: N.Nat.Le(1n+dp, x)) -> N.Nat.Le(1n+M.msub(x, 1n+dp), x):
  %msub_add(1n+dp, x, h) : N.Nat.Le(1n+M.msub(x, 1n+dp), _)
  N.Nat.le_add_l(dp, M.msub(x, 1n+dp))

# ---------------------------------------------------------------------
# 1b. mathlib's `mod` really is the remainder.
#
# `M.mod(x, d)` is `M.mod_go(x, x, d)`: subtract d while d <= x, with a
# fuel to keep the recursion structural. Two inductions on that fuel say
# what the answer means -- it is below d, and it completes a multiple of d
# to x. Everything about divisibility below is a corollary of these two.
# ---------------------------------------------------------------------

def le_zero_le(x: Nat, -dp: Nat, h: N.Nat.Le(x, 0n)) -> N.Nat.Le(x, dp):
  match x:
    case 0n:
      Unit{}
    case 1n+p:
      match h:

# one step of the remainder loop: the Bool `c` is the comparison, passed in
# as a parameter because a match cannot scrutinise a computed value
def mgo_lt.step(g: Nat, +x: Nat, +dp: Nat, c: Bool,
    +ec: {M.nat_le(1n+dp, x) == c : Bool},
    h: N.Nat.Le(x, 1n+g),
    rec: @y: Nat -> @hy: N.Nat.Le(y, g) -> N.Nat.Le(M.mod_go(g, y, 1n+dp), dp))
    -> N.Nat.Le(M.pick(Nat, c, M.mod_go(g, M.msub(x, 1n+dp), 1n+dp), x), dp):
  match c:
    case True{}:
      rec(M.msub(x, 1n+dp),
        N.Nat.le_trans(1n+M.msub(x, 1n+dp), x, 1n+g,
          msub_lt(x, dp, le_of_nat_le(1n+dp, x, ec)), h))
    case False{}:
      lt_of_nat_le_false(1n+dp, x, ec)

# the remainder is below the divisor
def mgo_lt(f: Nat, +x: Nat, +dp: Nat, h: N.Nat.Le(x, f)) -> N.Nat.Le(M.mod_go(f, x, 1n+dp), dp):
  match f:
    case 0n:
      le_zero_le(x, dp, h)
    case 1n+g:
      +g2 = g
      mgo_lt.step(g2, x, dp, M.nat_le(1n+dp, x), {==}, h, y => hy => mgo_lt(g2, y, dp, hy))

# quotient * divisor + remainder = input: the successor step
def mgo_eq.fin(+x: Nat, +dp: Nat, +s: Nat, +r: Nat, es: {Nat.add(1n+dp, s) == x : Nat},
    +q0: Nat, prf: {Nat.add(Nat.mul(q0, 1n+dp), r) == s : Nat})
    -> (&q: Nat -> {Nat.add(Nat.mul(q, 1n+dp), r) == x : Nat}):
  (1n+q0,
    %es : {Nat.add(Nat.mul(1n+q0, 1n+dp), r) == _ : Nat}
    %prf : {Nat.add(Nat.mul(1n+q0, 1n+dp), r) == Nat.add(1n+dp, _) : Nat}
    Equal.sym(Nat, Nat.add(1n+dp, Nat.add(Nat.mul(q0, 1n+dp), r)), Nat.add(Nat.add(1n+dp, Nat.mul(q0, 1n+dp)), r),
      N.Nat.add_assoc(1n+dp, Nat.mul(q0, 1n+dp), r)))

def mgo_eq.con(+x: Nat, +dp: Nat, +s: Nat, +r: Nat, es: {Nat.add(1n+dp, s) == x : Nat},
    w: (&q: Nat -> {Nat.add(Nat.mul(q, 1n+dp), r) == s : Nat}))
    -> (&q: Nat -> {Nat.add(Nat.mul(q, 1n+dp), r) == x : Nat}):
  (q0, prf) = w
  mgo_eq.fin(x, dp, s, r, es, q0, prf)

def mgo_eq.step(+g: Nat, +x: Nat, +dp: Nat, c: Bool,
    +ec: {M.nat_le(1n+dp, x) == c : Bool},
    h: N.Nat.Le(x, 1n+g),
    rec: @y: Nat -> @hy: N.Nat.Le(y, g) -> (&q: Nat -> {Nat.add(Nat.mul(q, 1n+dp), M.mod_go(g, y, 1n+dp)) == y : Nat}))
    -> (&q: Nat -> {Nat.add(Nat.mul(q, 1n+dp), M.pick(Nat, c, M.mod_go(g, M.msub(x, 1n+dp), 1n+dp), x)) == x : Nat}):
  match c:
    case True{}:
      mgo_eq.con(x, dp, M.msub(x, 1n+dp), M.mod_go(g, M.msub(x, 1n+dp), 1n+dp),
        msub_add(1n+dp, x, le_of_nat_le(1n+dp, x, ec)),
        rec(M.msub(x, 1n+dp),
          N.Nat.le_trans(1n+M.msub(x, 1n+dp), x, 1n+g,
            msub_lt(x, dp, le_of_nat_le(1n+dp, x, ec)), h)))
    case False{}:
      (0n, {==})

def mgo_eq(f: Nat, +x: Nat, +dp: Nat, h: N.Nat.Le(x, f))
    -> (&q: Nat -> {Nat.add(Nat.mul(q, 1n+dp), M.mod_go(f, x, 1n+dp)) == x : Nat}):
  match f:
    case 0n:
      (0n, {==})
    case 1n+g:
      +g2 = g
      mgo_eq.step(g2, x, dp, M.nat_le(1n+dp, x), {==}, h, y => hy => mgo_eq(g2, y, dp, hy))

# the two facts, at the fuel `mod` actually uses
def mod_lt(+x: Nat, +dp: Nat) -> N.Nat.Le(M.mod(x, 1n+dp), dp):
  mgo_lt(x, x, dp, N.Nat.le_refl(x))

def mod_eq(+x: Nat, +dp: Nat) -> (&q: Nat -> {Nat.add(Nat.mul(q, 1n+dp), M.mod(x, 1n+dp)) == x : Nat}):
  mgo_eq(x, x, dp, N.Nat.le_refl(x))

# ---------------------------------------------------------------------
# 1c. `M.divides(d, x) == True{}` and "some q has q*d = x" are the same
# thing, for every d >= 1. This is the hinge of the whole file: above it
# everything is Bools, below it everything is arithmetic.
# ---------------------------------------------------------------------

def divides_elim.fin(+dp: Nat, +x: Nat, r: Nat, hr: {r == 0n : Nat}, +q: Nat,
    prf: {Nat.add(Nat.mul(q, 1n+dp), r) == x : Nat}) -> P.Dvd(1n+dp, x):
  (q,
    %N.Nat.add_zero(Nat.mul(q, 1n+dp)) : {_ == x : Nat}
    %hr : {Nat.add(Nat.mul(q, 1n+dp), _) == x : Nat}
    prf)

def divides_elim.open(+dp: Nat, +x: Nat, r: Nat, hr: {r == 0n : Nat},
    w: (&q: Nat -> {Nat.add(Nat.mul(q, 1n+dp), r) == x : Nat})) -> P.Dvd(1n+dp, x):
  (q, prf) = w
  divides_elim.fin(dp, x, r, hr, q, prf)

# a True divisibility flag yields the quotient
def divides_elim(+dp: Nat, +x: Nat, e: {M.divides(1n+dp, x) == True{} : Bool}) -> P.Dvd(1n+dp, x):
  divides_elim.open(dp, x, M.mod(x, 1n+dp), eq_of_nat_eq(M.mod(x, 1n+dp), 0n, e), mod_eq(x, dp))

def divides_intro.fin(+dp: Nat, +x: Nat, +q: Nat, e: {Nat.mul(q, 1n+dp) == x : Nat}, +r: Nat,
    hr: N.Nat.Le(r, dp), +q0: Nat, prf: {Nat.add(Nat.mul(q0, 1n+dp), r) == x : Nat}) -> {r == 0n : Nat}:
  P.Nat.mul_rem_zero(q0, q, dp, r,
    Equal.trans(Nat, Nat.add(Nat.mul(q0, 1n+dp), r), x, Nat.mul(q, 1n+dp), prf,
      Equal.sym(Nat, Nat.mul(q, 1n+dp), x, e)),
    hr)

def divides_intro.open(+dp: Nat, +x: Nat, +q: Nat, e: {Nat.mul(q, 1n+dp) == x : Nat}, +r: Nat,
    hr: N.Nat.Le(r, dp),
    w: (&q0: Nat -> {Nat.add(Nat.mul(q0, 1n+dp), r) == x : Nat})) -> {r == 0n : Nat}:
  (q0, prf) = w
  divides_intro.fin(dp, x, q, e, r, hr, q0, prf)

# an exact quotient makes the flag True
def divides_intro(+dp: Nat, +x: Nat, +q: Nat, e: {Nat.mul(q, 1n+dp) == x : Nat}) -> {M.divides(1n+dp, x) == True{} : Bool}:
  nat_eq_of_eq(M.mod(x, 1n+dp), 0n,
    divides_intro.open(dp, x, q, e, M.mod(x, 1n+dp), mod_lt(x, dp), mod_eq(x, dp)))

def divides_of_dvd(+dp: Nat, +x: Nat, w: P.Dvd(1n+dp, x)) -> {M.divides(1n+dp, x) == True{} : Bool}:
  P.Dvd.open(1n+dp, x, w, {M.divides(1n+dp, x) == True{} : Bool}, q => e => divides_intro(dp, x, q, e))

# divisibility composes: a divisor of a divisor of x divides x
def divides_chain(+ep: Nat, +pp: Nat, +x: Nat,
    hep: {M.divides(1n+ep, 1n+pp) == True{} : Bool},
    hpx: {M.divides(1n+pp, x) == True{} : Bool}) -> {M.divides(1n+ep, x) == True{} : Bool}:
  divides_of_dvd(ep, x,
    P.Dvd.trans(1n+ep, 1n+pp, x, divides_elim(ep, 1n+pp, hep), divides_elim(pp, x, hpx)))

# ---------------------------------------------------------------------
# 2. mathlib's trial division `has_divisor(x, k)` = "some d with
# 2 <= d <= k divides x", in the direction the argument needs.
# ---------------------------------------------------------------------

# a divisor of x that is at least 2 and at most k makes the scan say True
def hd_intro(k: Nat, +dp: Nat, +x: Nat, +hd: {M.divides(2n+dp, x) == True{} : Bool},
    hle: N.Nat.Le(2n+dp, k)) -> {M.has_divisor(x, k) == True{} : Bool}:
  match k:
    case 0n:
      match hle:
    case 1n:
      match hle:
    case 2n+q:
      +q2 = q
      P.Nat.le_split(dp, q2, hle, {M.has_divisor(x, 2n+q2) == True{} : Bool},
        eqd =>
          %eqd : {Bool.or(M.divides(2n+_, x), M.has_divisor(x, 1n+_)) == True{} : Bool}
          %Equal.sym(Bool, M.divides(2n+dp, x), True{}, hd) : {Bool.or(_, M.has_divisor(x, 1n+dp)) == True{} : Bool}
          {==},
        ltd =>
          %Equal.sym(Bool, M.has_divisor(x, 1n+q2), True{}, hd_intro(1n+q2, dp, x, hd, ltd)) : {Bool.or(M.divides(2n+q2, x), _) == True{} : Bool}
          M.or_true(M.divides(2n+q2, x)))

# ---------------------------------------------------------------------
# 3. the scan, and why its answer is prime.
#
# `scan` walks d = 2, 3, ... upward through x carrying mathlib's own
# "nothing from 2 to d-1 divides x" as a Bool equation, and stops at the
# first d that divides x. The invariant is the whole point: what comes out
# is not just a divisor but the LEAST one, in exactly the form
# `M.is_prime` will need.
# ---------------------------------------------------------------------

# the package the scan returns: p = 2+pp divides x, and nothing below it does
def Least(x: Nat, pp: Nat) -> Type:
  {M.divides(2n+pp, x) == True{} : Bool} & {M.has_divisor(x, 1n+pp) == False{} : Bool}

def Found(x: Nat) -> Type:
  &pp: Nat -> Least(x, pp)

# a divisor of the least divisor would be a smaller divisor of x, so there
# is none: the Bool test for it is False
def not_div_p(+q: Nat, +pp: Nat, +x: Nat, c: Bool,
    ec: {M.divides(2n+q, 2n+pp) == c : Bool},
    hdvp: {M.divides(2n+pp, x) == True{} : Bool},
    hnd: {M.has_divisor(x, 1n+pp) == False{} : Bool},
    hle: N.Nat.Le(2n+q, 1n+pp)) -> {M.divides(2n+q, 2n+pp) == False{} : Bool}:
  match c:
    case True{}:
      Empty.absurd({M.divides(2n+q, 2n+pp) == False{} : Bool},
        N.Bool.true_ne_false(
          Equal.trans(Bool, True{}, M.has_divisor(x, 1n+pp), False{},
            Equal.sym(Bool, M.has_divisor(x, 1n+pp), True{},
              hd_intro(1n+pp, q, x, divides_chain(1n+q, 1n+pp, x, ec, hdvp), hle)),
            hnd)))
    case False{}:
      ec

# so trial division on the least divisor itself finds nothing, at every k
# up to p-1 -- which is `M.is_prime(p)` once k reaches p-1
def least_no_divisor(k: Nat, +pp: Nat, +x: Nat,
    +hdvp: {M.divides(2n+pp, x) == True{} : Bool},
    +hnd: {M.has_divisor(x, 1n+pp) == False{} : Bool},
    hle: N.Nat.Le(k, 1n+pp)) -> {M.has_divisor(2n+pp, k) == False{} : Bool}:
  match k:
    case 0n:
      {==}
    case 1n:
      {==}
    case 2n+q:
      +q2 = q
      P.Nat.le_copy(2n+q2, 1n+pp, hle, {M.has_divisor(2n+pp, 2n+q2) == False{} : Bool}, h1 => h2 =>
        %Equal.sym(Bool, M.has_divisor(2n+pp, 1n+q2), False{},
          least_no_divisor(1n+q2, pp, x, hdvp, hnd, N.Nat.lt_le(q2, pp, h1))) : {Bool.or(M.divides(2n+q2, 2n+pp), _) == False{} : Bool}
        %Equal.sym(Bool, M.divides(2n+q2, 2n+pp), False{},
          not_div_p(q2, pp, x, M.divides(2n+q2, 2n+pp), {==}, hdvp, hnd, h2)) : {Bool.or(_, False{}) == False{} : Bool}
        {==})

# one step of the scan: the divisibility flag arrives as a parameter,
# because a match cannot scrutinise a computed value
def scan.step(+g: Nat, +x: Nat, +dp: Nat, c: Bool,
    ec: {M.divides(2n+dp, x) == c : Bool},
    hnd: {M.has_divisor(x, 1n+dp) == False{} : Bool},
    hb: {Nat.add(2n+dp, 1n+g) == x : Nat},
    rec: @dq: Nat -> @h1: {M.has_divisor(x, 1n+dq) == False{} : Bool} -> @h2: {Nat.add(2n+dq, g) == x : Nat} -> Found(x)) -> Found(x):
  match c:
    case True{}:
      (dp, (ec, hnd))
    case False{}:
      rec(1n+dp,
        %Equal.sym(Bool, M.has_divisor(x, 1n+dp), False{}, hnd) : {Bool.or(M.divides(2n+dp, x), _) == False{} : Bool}
        %Equal.sym(Bool, M.divides(2n+dp, x), False{}, ec) : {Bool.or(_, False{}) == False{} : Bool}
        {==},
        Equal.trans(Nat, 3n+Nat.add(dp, g), Nat.add(2n+dp, 1n+g), x,
          Equal.cong(Nat, Nat, z => 2n+z, 1n+Nat.add(dp, g), Nat.add(dp, 1n+g),
            Equal.sym(Nat, Nat.add(dp, 1n+g), 1n+Nat.add(dp, g), N.Nat.add_succ(dp, g))),
          hb))

# the fuel runs out exactly at d = x, and x always divides itself
def scan.done(+x: Nat, +dp: Nat,
    hnd: {M.has_divisor(x, 1n+dp) == False{} : Bool},
    hb: {Nat.add(2n+dp, 0n) == x : Nat}) -> Found(x):
  (dp,
    (divides_intro(1n+dp, x, 1n,
       Equal.trans(Nat, Nat.mul(1n, 2n+dp), 2n+dp, x,
         N.Nat.one_mul(2n+dp),
         Equal.trans(Nat, 2n+dp, Nat.add(2n+dp, 0n), x,
           Equal.sym(Nat, Nat.add(2n+dp, 0n), 2n+dp, N.Nat.add_zero(2n+dp)),
           hb))),
     hnd))

# the least divisor above 1 of x, found by walking up from 2. The fuel is
# tied to the value by `2 + dp + f = x`, so it cannot run out early.
def scan(f: Nat, +x: Nat, +dp: Nat,
    hnd: {M.has_divisor(x, 1n+dp) == False{} : Bool},
    hb: {Nat.add(2n+dp, f) == x : Nat}) -> Found(x):
  match f:
    case 0n:
      scan.done(x, dp, hnd, hb)
    case 1n+g:
      +g2 = g
      scan.step(g2, x, dp, M.divides(2n+dp, x), {==}, hnd, hb,
        dq => h1 => h2 => scan(g2, x, dq, h1, h2))

# ---------------------------------------------------------------------
# 4. Euclid's theorem
# ---------------------------------------------------------------------

def Euclid(n: Nat) -> Type:
  &p: Nat -> {Bool.and(M.nat_le(n, p), M.is_prime(p)) == True{} : Bool}

# `M.is_prime(2+pp)` unfolds to "2 <= 2+pp" (immediate) and "trial
# division up to (2+pp)-1 = 1+pp finds nothing", which is
# `least_no_divisor` at k = 1+pp.
def least_is_prime(+pp: Nat, +x: Nat,
    hdv: {M.divides(2n+pp, x) == True{} : Bool},
    hn: {M.has_divisor(x, 1n+pp) == False{} : Bool}) -> {M.is_prime(2n+pp) == True{} : Bool}:
  %Equal.sym(Bool, M.has_divisor(2n+pp, 1n+pp), False{},
    least_no_divisor(1n+pp, pp, x, hdv, hn, N.Nat.le_refl(1n+pp))) : {Bool.not(_) == True{} : Bool}
  {==}

# with p = 2+pp the least divisor of n!+1 in hand: either n <= p, and we
# are done, or p < n -- and then p divides n! as well as n!+1, which no
# number above 1 can do.
def euclid.fin(+n: Nat, +m: Nat, +hf: {P.fact(n) == 1n+m : Nat}, +pp: Nat,
    +hdv: {M.divides(2n+pp, 2n+m) == True{} : Bool},
    hn: {M.has_divisor(2n+m, 1n+pp) == False{} : Bool}) -> Euclid(n):
  P.Nat.le_total(n, 2n+pp, Euclid(n),
    hle =>
      (2n+pp,
        %Equal.sym(Bool, M.nat_le(n, 2n+pp), True{}, nat_le_of_le(n, 2n+pp, hle)) : {Bool.and(_, M.is_prime(2n+pp)) == True{} : Bool}
        %Equal.sym(Bool, M.is_prime(2n+pp), True{}, least_is_prime(pp, 2n+m, hdv, hn)) : {Bool.and(True{}, _) == True{} : Bool}
        {==}),
    hgt =>
      Empty.absurd(Euclid(n),
        P.Dvd.consecutive(pp, P.fact(n),
          P.fact_div(n, 1n+pp, N.Nat.lt_le(2n+pp, n, hgt)),
          %Equal.sym(Nat, P.fact(n), 1n+m, hf) : P.Dvd(2n+pp, 1n+_)
          divides_elim(1n+pp, 2n+m, hdv))))

def euclid.found(+n: Nat, +m: Nat, +hf: {P.fact(n) == 1n+m : Nat}, +pp: Nat, w: Least(2n+m, pp)) -> Euclid(n):
  (hdv, hn) = w
  euclid.fin(n, m, hf, pp, hdv, hn)

def euclid.open2(+n: Nat, +m: Nat, +hf: {P.fact(n) == 1n+m : Nat}, w: Found(2n+m)) -> Euclid(n):
  (pp, w2) = w
  euclid.found(n, m, hf, pp, w2)

# n! + 1 is 2 + m, so the scan starts at d = 2 with fuel m and the
# invariant "nothing up to 1 divides it", which is True by definition.
def euclid.start(+n: Nat, +m: Nat, +hf: {P.fact(n) == 1n+m : Nat}) -> Euclid(n):
  euclid.open2(n, m, hf, scan(m, 2n+m, 0n, {==}, {==}))

def euclid.open1(+n: Nat, w: (&m: Nat -> {P.fact(n) == 1n+m : Nat})) -> Euclid(n):
  (m, hf) = w
  euclid.start(n, m, hf)

# THE THEOREM: for every n there is a p with n <= p and p prime.
def no_largest_prime(n: Nat) -> (&p: Nat -> {Bool.and(M.nat_le(n, p), M.is_prime(p)) == True{} : Bool}):
  +n2 = n
  euclid.open1(n2, P.fact_pos(n2))