Inverse.inv_dvd_a2: 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 163-165 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=163&end_line=165

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/gcd.bend as G

def inv_dvd_a2(+a: Nat, +mp: Nat, +g: Nat, +w: G.Wit, p: G.divides_both(1n+mp, Nat.mod(a, 1n+mp), g, w)) -> {a == Nat.mul(Nat.add(Nat.mul(Nat.div(a, 1n+mp), G.wl(w)), G.wr(w)), g) : Nat}:
  (en, er) = p
  G.dvd_of_mod(mp, a, g, G.wl(w), G.wr(w), en, er)

Uses (11):
  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.div
  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=Sigma
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/gcd.bend&name=Wit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/gcd.bend&name=divides_both
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/gcd.bend&name=dvd_of_mod
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/gcd.bend&name=wl
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/gcd.bend&name=wr