def inv_km

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/inverse.bend:150

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

150# the final remainder divides m and a
151def inv_km(+a: Nat, +mp: Nat) -> Nat:
152  G.wl(G.ws(1n+mp, 1n+mp, Nat.mod(a, 1n+mp)))