Cong.c_cancel: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as Cong
Lines 93-106 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend&start_line=93&end_line=106

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR

# X + m == Y + m (mod p) -> X == Y (mod p): add p - (m mod p) to both
def c_cancel(+pp: Nat, +X: Nat, +Y: Nat, +m: Nat, +h: ceq(pp, Nat.add(X, m), Nat.add(Y, m))) -> ceq(pp, X, Y):
  +P = {1n+pp : Nat}
  +q = Nat.div(m, P)
  +r = Nat.mod(m, P)
  +t = Nat.sub(P, r)
  +hm = NR.dm_eq(pp, m)
  +hrt = N.sub_add(P, r, N.lt_le(r, P, NR.dm_lt(pp, m)))
  +k = Nat.add(Nat.mul(q, P), P)
  +hk = Equal.trans(Nat, Nat.add(m, t), Nat.add(Nat.add(Nat.mul(q, P), r), t), k, Equal.cong(Nat, Nat, z => Nat.add(z, t), m, Nat.add(Nat.mul(q, P), r), hm), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(q, P), r), t), Nat.add(Nat.mul(q, P), Nat.add(r, t)), k, NA.add_assoc(Nat.mul(q, P), r, t), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(q, P), z), Nat.add(r, t), P, hrt)))
  +hk2 = Equal.trans(Nat, Nat.add(m, t), k, Nat.mul(1n+q, P), hk, NA.add_comm(Nat.mul(q, P), P))
  +ex = c_trans(pp, X, Nat.add(Nat.mul(1n+q, P), X), Nat.add(Nat.add(X, m), t), c_sym(pp, Nat.add(Nat.mul(1n+q, P), X), X, NR.absorb(pp, 1n+q, X)), c_eq(pp, Nat.add(Nat.mul(1n+q, P), X), Nat.add(Nat.add(X, m), t), Equal.sym(Nat, Nat.add(Nat.add(X, m), t), Nat.add(Nat.mul(1n+q, P), X), shift3(X, m, t, Nat.mul(1n+q, P), hk2))))
  +ey = c_trans(pp, Nat.add(Nat.add(Y, m), t), Nat.add(Nat.mul(1n+q, P), Y), Y, c_eq(pp, Nat.add(Nat.add(Y, m), t), Nat.add(Nat.mul(1n+q, P), Y), shift3(Y, m, t, Nat.mul(1n+q, P), hk2)), NR.absorb(pp, 1n+q, Y))
  c_trans(pp, X, Nat.add(Nat.add(X, m), t), Y, ex, c_trans(pp, Nat.add(Nat.add(X, m), t), Nat.add(Nat.add(Y, m), t), Y, c_add(pp, Nat.add(X, m), Nat.add(Y, m), t, t, h, c_refl(pp, t)), ey))

Uses (23):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend&name=c_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend&name=c_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend&name=c_refl
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend&name=c_sym
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend&name=c_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend&name=ceq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend&name=shift3
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=sub_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=absorb
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=dm_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=dm_lt