~/jendhub

def inverse_fail

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

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/src/math/natural.bend as M

198# mod_inverse(a, m) == Fail{NotInvertible}: g >= 2 divides a and m, so a
199# and m are not coprime   (Mathlib Nat.Coprime, ZMod.unitOfCoprime)
200def inverse_fail(+a: Nat, +mp: Nat, +h: {M.mod_inverse(a, 1n+mp) == Fail{M.NotInvertible{}} : Result<&2, &2, M.MathError, Nat>}) -> {Nat.is_le(2n, bg(inv_bz(a, mp))) == True{} : Bool} & ({a == Nat.mul(inv_ka(a, mp), bg(inv_bz(a, mp))) : Nat} & {1n+mp == Nat.mul(inv_km(a, mp), bg(inv_bz(a, mp))) : Nat}):
201  (fail_bz(mp, inv_bz(a, mp), inv_km(a, mp), inv_dvd_m(a, mp), h), (inv_dvd_a(a, mp), inv_dvd_m(a, mp)))

Uses (16)

Used by (1)