Inverse.inverse_fail: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/inverse.bend as Inverse
Lines 198-201 of bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/inverse.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/inverse.bend&start_line=198&end_line=201

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M

# mod_inverse(a, m) == Fail{NotInvertible}: g >= 2 divides a and m, so a
# and m are not coprime   (Mathlib Nat.Coprime, ZMod.unitOfCoprime)
def inverse_fail(+a: Nat, +mp: Nat, +h: {M.mod_inverse(a, 1n+mp) == Fail{M.NotInvertible{}} : Result<&2, &2, M.MathError, Nat>}) -> {Nat.is_le(2n, bg(inv_bz(a, mp))) == True{} : Bool} & ({a == Nat.mul(inv_ka(a, mp), bg(inv_bz(a, mp))) : Nat} & {1n+mp == Nat.mul(inv_km(a, mp), bg(inv_bz(a, mp))) : Nat}):
  (fail_bz(mp, inv_bz(a, mp), inv_km(a, mp), inv_dvd_m(a, mp), h), (inv_dvd_a(a, mp), inv_dvd_m(a, mp)))

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/inverse.bend&name=bg
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/inverse.bend&name=fail_bz
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/inverse.bend&name=inv_bz
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/inverse.bend&name=inv_dvd_a
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/inverse.bend&name=inv_dvd_m
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/inverse.bend&name=inv_ka
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/inverse.bend&name=inv_km
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend&name=MathError
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend&name=mod_inverse