Eqf.eq_bool: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/eqf.bend as Eqf
Lines 74-80 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/eqf.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/eqf.bend&start_line=74&end_line=80

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N

def eq_bool(+pp: Nat, +A: Nat, +B: Nat, +hA: {Nat.is_lt(A, 1n+pp) == True{} : Bool}, +hB: {Nat.is_lt(B, 1n+pp) == True{} : Bool}, +b: Bool, +hb: {Nat.is_eq(A, B) == b : Bool}) -> {Nat.is_eq(Nat.mod(pw(pp, A, B), 1n+pp), 0n) == Nat.is_eq(A, B) : Bool}:
  match b:
    case True{}:
      +e = N.eq_from_is_eq(A, B, hb)
      Equal.trans(Bool, Nat.is_eq(Nat.mod(pw(pp, A, B), 1n+pp), 0n), True{}, Nat.is_eq(A, B), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), Nat.mod(pw(pp, A, B), 1n+pp), 0n, w_zero(pp, A, B, hB, e)), Equal.sym(Bool, Nat.is_eq(A, B), True{}, hb))
    case False{}:
      eq_false(pp, A, B, hA, hB, hb, Nat.is_eq(Nat.mod(pw(pp, A, B), 1n+pp), 0n), {==})

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=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.is_eq
  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-crypto@1.0.0.0/proofs/crypto/curve25519/eqf.bend&name=eq_false
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/eqf.bend&name=pw
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/eqf.bend&name=w_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=eq_from_is_eq