Top.x_ge2: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend as Top
Lines 73-81 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend&start_line=73&end_line=81

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR

# 8p <= m gives X >= 2.
def x_ge2(+m: Nat, +p: Nat, +hp: {Nat.is_le(1n, p) == True{} : Bool}, +h8: {Nat.is_le(Nat.mul(8n, p), m) == True{} : Bool}) -> {Nat.is_le(2n, X(m, p)) == True{} : Bool}:
  match p:
    case 0n:
      Empty.absurd({Nat.is_le(2n, X(m, 0n)) == True{} : Bool}, L.false_true(hp))
    case 1n+ +b:
      +e = NR.le_div(Nat.add(b, Nat.mul(3n, 1n+b)), 2n, m)
      +h2 = L.subst(Nat, z => {Nat.is_le(z, m) == True{} : Bool}, Nat.mul(8n, 1n+b), Nat.mul(2n, Nat.mul(4n, 1n+b)), NA.mul_assoc(2n, 4n, 1n+b), h8)
      Equal.trans(Bool, Nat.is_le(2n, X(m, 1n+b)), Nat.is_le(Nat.mul(2n, Nat.mul(4n, 1n+b)), m), True{}, e, h2)

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  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_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend&name=X
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=false_true
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=le_div