def inv_ka

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

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

154def inv_ka(+a: Nat, +mp: Nat) -> Nat:
155  Nat.add(Nat.mul(Nat.div(a, 1n+mp), inv_km(a, mp)), G.wr(G.ws(1n+mp, 1n+mp, Nat.mod(a, 1n+mp))))