Cong.c_subm: 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 111-121 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=111&end_line=121

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

# (X + p) - m == (Y + p) - m (mod p) for X == Y (mod p) and m <= p
def c_subm(+pp: Nat, +X: Nat, +Y: Nat, +m: Nat, +h: ceq(pp, X, Y), +hm: {Nat.is_le(m, 1n+pp) == True{} : Bool}) -> ceq(pp, Nat.sub(Nat.add(X, 1n+pp), m), Nat.sub(Nat.add(Y, 1n+pp), m)):
  +P = {1n+pp : Nat}
  +X2 = Nat.sub(Nat.add(X, P), m)
  +Y2 = Nat.sub(Nat.add(Y, P), m)
  +mx = N.le_trans(m, P, Nat.add(X, P), hm, le_add_l(X, P))
  +my = N.le_trans(m, P, Nat.add(Y, P), hm, le_add_l(Y, P))
  +ex = Equal.trans(Nat, Nat.add(X2, m), Nat.add(m, X2), Nat.add(X, P), NA.add_comm(X2, m), N.sub_add(Nat.add(X, P), m, mx))
  +ey = Equal.trans(Nat, Nat.add(Y2, m), Nat.add(m, Y2), Nat.add(Y, P), NA.add_comm(Y2, m), N.sub_add(Nat.add(Y, P), m, my))
  +e = c_trans(pp, Nat.add(X2, m), Nat.add(X, P), Nat.add(Y2, m), c_eq(pp, Nat.add(X2, m), Nat.add(X, P), ex), c_trans(pp, Nat.add(X, P), Nat.add(Y, P), Nat.add(Y2, m), c_add(pp, X, Y, P, P, h, c_refl(pp, P)), c_eq(pp, Nat.add(Y, P), Nat.add(Y2, m), Equal.sym(Nat, Nat.add(Y2, m), Nat.add(Y, P), ey))))
  c_cancel(pp, X2, Y2, m, e)

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.is_le
  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_cancel
  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_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=le_add_l
  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=le_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=sub_add