Eqf.eq_false: 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 64-72 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=64&end_line=72

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

def eq_false(+pp: Nat, +A: Nat, +B: Nat, +hA: {Nat.is_lt(A, 1n+pp) == True{} : Bool}, +hB: {Nat.is_lt(B, 1n+pp) == True{} : Bool}, +hb: {Nat.is_eq(A, B) == False{} : Bool}, +c: Bool, +hc: {Nat.is_eq(Nat.mod(pw(pp, A, B), 1n+pp), 0n) == c : Bool}) -> {Nat.is_eq(Nat.mod(pw(pp, A, B), 1n+pp), 0n) == Nat.is_eq(A, B) : Bool}:
  match c:
    case True{}:
      +m = Nat.mod(pw(pp, A, B), 1n+pp)
      +e = w_ne(pp, A, B, hA, hB, N.eq_from_is_eq(m, 0n, hc))
      Empty.absurd({Nat.is_eq(m, 0n) == Nat.is_eq(A, B) : Bool}, L.true_not_false(Nat.is_eq(A, B), L.subst(Nat, z => {Nat.is_eq(A, z) == True{} : Bool}, A, B, e, N.is_eq_refl(A)), hb))
    case False{}:
      +m = Nat.mod(pw(pp, A, B), 1n+pp)
      Equal.trans(Bool, Nat.is_eq(m, 0n), False{}, Nat.is_eq(A, B), hc, Equal.sym(Bool, Nat.is_eq(A, B), False{}, hb))

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