def c_cancel

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/cong.bend:93

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

93# X + m == Y + m (mod p) -> X == Y (mod p): add p - (m mod p) to both
94def 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):
95  +P = {1n+pp : Nat}
96  +q = Nat.div(m, P)
97  +r = Nat.mod(m, P)
98  +t = Nat.sub(P, r)
99  +hm = NR.dm_eq(pp, m)
100  +hrt = N.sub_add(P, r, N.lt_le(r, P, NR.dm_lt(pp, m)))
101  +k = Nat.add(Nat.mul(q, P), P)
102  +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)))
103  +hk2 = Equal.trans(Nat, Nat.add(m, t), k, Nat.mul(1n+q, P), hk, NA.add_comm(Nat.mul(q, P), P))
104  +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))))
105  +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))
106  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))