def done_bz

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

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as R

174def done_bz(+mp: Nat, +a: Nat, +bz: M.Bezout, +hinv: {Nat.mod(Nat.mul(a, bc(bz)), 1n+mp) == Nat.mod(bg(bz), 1n+mp) : Nat}, +x: Nat, +h: {M.inv_fin(1n+mp, bz) == Done{x} : Result<&2, &2, M.MathError, Nat>}) -> {Nat.mod(Nat.mul(a, x), 1n+mp) == Nat.mod(1n, 1n+mp) : Nat} & {Nat.is_lt(x, 1n+mp) == True{} : Bool}:
175  match bz:
176    case M.BZ{0n, +s}:
177      Empty.absurd({Nat.mod(Nat.mul(a, x), 1n+mp) == Nat.mod(1n, 1n+mp) : Nat} & {Nat.is_lt(x, 1n+mp) == True{} : Bool}, L.false_true(Equal.cong(Result<&2, &2, M.MathError, Nat>, Bool, is_done, Fail{M.NotInvertible{}}, Done{x}, h)))
178    case M.BZ{1n, +s}:
179      +ex = Equal.cong(Result<&2, &2, M.MathError, Nat>, Nat, unwrap, Done{Nat.mod(s, 1n+mp)}, Done{x}, h)
180      %Equal.sym(Nat, x, Nat.mod(s, 1n+mp), Equal.sym(Nat, Nat.mod(s, 1n+mp), x, ex)) : {Nat.mod(Nat.mul(a, _), 1n+mp) == Nat.mod(1n, 1n+mp) : Nat} & {Nat.is_lt(_, 1n+mp) == True{} : Bool}
181      (Equal.trans(Nat, Nat.mod(Nat.mul(a, Nat.mod(s, 1n+mp)), 1n+mp), Nat.mod(Nat.mul(a, s), 1n+mp), Nat.mod(1n, 1n+mp), R.mod_mul_r(mp, a, s), hinv), R.dm_lt(mp, s))
182    case M.BZ{2n+gg, +s}:
183      Empty.absurd({Nat.mod(Nat.mul(a, x), 1n+mp) == Nat.mod(1n, 1n+mp) : Nat} & {Nat.is_lt(x, 1n+mp) == True{} : Bool}, L.false_true(Equal.cong(Result<&2, &2, M.MathError, Nat>, Bool, is_done, Fail{M.NotInvertible{}}, Done{x}, h)))