def sub_mod

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/negate.bend:173

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

173# a + (m - b) = (a + m) - b, for b < m
174def sub_mod(+mp: Nat, +a: Nat, +b: Nat, +nb: Nat, +hlt: {Nat.is_lt(b, 1n+mp) == True{} : Bool}, +hn: {Nat.add(nb, b) == 1n+mp : Nat}) -> {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(Nat.add(a, 1n+mp), Nat.mod(b, 1n+mp)), 1n+mp) : Nat}:
175  %Equal.sym(Nat, Nat.mod(b, 1n+mp), b, NR.mod_of(0n, mp, b, hlt)) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(Nat.add(a, 1n+mp), _), 1n+mp) : Nat}
176  %Equal.sym(Nat, 1n+mp, Nat.add(nb, b), Equal.sym(Nat, Nat.add(nb, b), 1n+mp, hn)) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(Nat.add(a, _), b), 1n+mp) : Nat}
177  %Equal.sym(Nat, Nat.add(a, Nat.add(nb, b)), Nat.add(Nat.add(a, nb), b), Equal.sym(Nat, Nat.add(Nat.add(a, nb), b), Nat.add(a, Nat.add(nb, b)), NA.add_assoc(a, nb, b))) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(_, b), 1n+mp) : Nat}
178  %Equal.sym(Nat, Nat.add(Nat.add(a, nb), b), Nat.add(b, Nat.add(a, nb)), NA.add_comm(Nat.add(a, nb), b)) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(_, b), 1n+mp) : Nat}
179  %Equal.sym(Nat, Nat.sub(Nat.add(b, Nat.add(a, nb)), b), Nat.add(a, nb), N.add_sub_cancel(b, Nat.add(a, nb))) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(_, 1n+mp) : Nat}
180  {==}