def c_subm

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

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

111# (X + p) - m == (Y + p) - m (mod p) for X == Y (mod p) and m <= p
112def 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)):
113  +P = {1n+pp : Nat}
114  +X2 = Nat.sub(Nat.add(X, P), m)
115  +Y2 = Nat.sub(Nat.add(Y, P), m)
116  +mx = N.le_trans(m, P, Nat.add(X, P), hm, le_add_l(X, P))
117  +my = N.le_trans(m, P, Nat.add(Y, P), hm, le_add_l(Y, P))
118  +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))
119  +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))
120  +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))))
121  c_cancel(pp, X2, Y2, m, e)