Inverse.fail_bz: 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 189-196 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=189&end_line=196

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
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend as LC

def fail_bz(+mp: Nat, +bz: M.Bezout, +km: Nat, +em: {1n+mp == Nat.mul(km, bg(bz)) : Nat}, +h: {M.inv_fin(1n+mp, bz) == Fail{M.NotInvertible{}} : Result<&2, &2, M.MathError, Nat>}) -> {Nat.is_le(2n, bg(bz)) == True{} : Bool}:
  match bz:
    case M.BZ{0n, s}:
      Empty.absurd({Nat.is_le(2n, 0n) == True{} : Bool}, L.false_true(LC.gcd_pos(mp, km, 0n, em)))
    case M.BZ{1n, s}:
      Empty.absurd({Nat.is_le(2n, 1n) == True{} : Bool}, L.false_true(Equal.sym(Bool, True{}, False{}, Equal.cong(Result<&2, &2, M.MathError, Nat>, Bool, is_done, Done{Nat.mod(s, 1n+mp)}, Fail{M.NotInvertible{}}, h))))
    case M.BZ{2n+ +gg, s}:
      N.le_add_right(2n, gg)

Uses (17):
  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.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=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.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  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/nat.bend&name=le_add_right
  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=is_done
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend&name=gcd_pos
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend&name=Bezout
  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=inv_fin