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

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as R
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/gcd.bend as G

def inv_dvd_a(+a: Nat, +mp: Nat) -> {a == Nat.mul(inv_ka(a, mp), bg(inv_bz(a, mp))) : Nat}:
  +m = {1n+mp : Nat}
  +g = M.gcd_go(m, m, Nat.mod(a, m))
  +w = G.ws(m, m, Nat.mod(a, m))
  %Equal.sym(Nat, bg(inv_bz(a, mp)), g, inv_r(m, m, m, 0n, Nat.mod(a, m), 1n)) : {a == Nat.mul(inv_ka(a, mp), _) : Nat}
  inv_dvd_a2(a, mp, g, w, G.gcd_both(m, m, Nat.mod(a, m), N.lt_le(Nat.mod(a, m), m, R.dm_lt(mp, a))))

Uses (14):
  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.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend&name=dm_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/gcd.bend&name=gcd_both
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/gcd.bend&name=ws
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/inverse.bend&name=bg
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/inverse.bend&name=inv_bz
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/inverse.bend&name=inv_dvd_a2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/inverse.bend&name=inv_ka
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/inverse.bend&name=inv_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/natural.bend&name=gcd_go