def inv_bezout

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

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as R

144def inv_bezout(+a: Nat, +mp: Nat) -> {Nat.mod(Nat.mul(a, bc(inv_bz(a, mp))), 1n+mp) == Nat.mod(bg(inv_bz(a, mp)), 1n+mp) : Nat}:
145  +m = {1n+mp : Nat}
146  +h0 = Equal.trans(Nat, Nat.mod(Nat.mul(a, 0n), m), 0n, Nat.mod(m, m), Equal.cong(Nat, Nat, z => Nat.mod(z, m), Nat.mul(a, 0n), 0n, A.mul_zero(a)), Equal.sym(Nat, Nat.mod(m, m), 0n, mod_self(mp)))
147  +h1 = Equal.trans(Nat, Nat.mod(Nat.mul(a, 1n), m), Nat.mod(a, m), Nat.mod(Nat.mod(a, m), m), Equal.cong(Nat, Nat, z => Nat.mod(z, m), Nat.mul(a, 1n), a, A.mul_one(a)), Equal.sym(Nat, Nat.mod(Nat.mod(a, m), m), Nat.mod(a, m), R.mod_mod(mp, a)))
148  inv_inv(m, mp, a, m, 0n, Nat.mod(a, m), 1n, h0, h1)