def inv_dvd_a2
bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/inverse.bend:163
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/inverse.bend as Inverse
import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/gcd.bend as G
163def 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}:
164 (en, er) = p
165 G.dvd_of_mod(mp, a, g, G.wl(w), G.wr(w), en, er)