Reduce.canon1_val: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reduce.bend as Reduce
Lines 200-219 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reduce.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reduce.bend&start_line=200&end_line=219

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
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend as SR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as I

# v + cv = lo + t with t = m + cv, v < t, cv + cv < t: v mod m = lo
def canon1_val(+mp: Nat, +v: Nat, +cv: Nat, +lo: Nat, +t: Nat, +ht: {Nat.add(1n+mp, cv) == t : Nat}, +hv: {Nat.is_lt(v, t) == True{} : Bool}, +hcc: {Nat.is_lt(Nat.add(cv, cv), t) == True{} : Bool}, +eu: {Nat.add(v, cv) == Nat.add(lo, t) : Nat}) -> {lo == Nat.mod(v, 1n+mp) : Nat}:
  +m = {1n+mp : Nat}
  # v = lo + m
  +e1 = Equal.trans(Nat, Nat.add(v, cv), Nat.add(lo, t), Nat.add(Nat.add(lo, m), cv), eu, Equal.trans(Nat, Nat.add(lo, t), Nat.add(lo, Nat.add(m, cv)), Nat.add(Nat.add(lo, m), cv), Equal.cong(Nat, Nat, z => Nat.add(lo, z), t, Nat.add(m, cv), Equal.sym(Nat, Nat.add(m, cv), t, ht)), Equal.sym(Nat, Nat.add(Nat.add(lo, m), cv), Nat.add(lo, Nat.add(m, cv)), NA.add_assoc(lo, m, cv))))
  +e2 = NR.add_cancel(cv, v, Nat.add(lo, m), Equal.trans(Nat, Nat.add(cv, v), Nat.add(v, cv), Nat.add(cv, Nat.add(lo, m)), NA.add_comm(cv, v), Equal.trans(Nat, Nat.add(v, cv), Nat.add(Nat.add(lo, m), cv), Nat.add(cv, Nat.add(lo, m)), e1, NA.add_comm(Nat.add(lo, m), cv))))
  # lo < cv < m
  +s1 = I.lt_subst_l(v, Nat.add(lo, m), t, e2, hv)
  +s2 = I.lt_subst_r(Nat.add(lo, m), t, Nat.add(cv, m), Equal.trans(Nat, t, Nat.add(m, cv), Nat.add(cv, m), Equal.sym(Nat, Nat.add(m, cv), t, ht), NA.add_comm(m, cv)), s1)
  +s3 = Equal.trans(Bool, Nat.is_lt(lo, cv), Nat.is_lt(Nat.add(lo, m), Nat.add(cv, m)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(lo, m), Nat.add(cv, m)), Nat.is_lt(lo, cv), WW.lt_cancel_r(lo, cv, m)), s2)
  +s4 = I.lt_subst_r(Nat.add(cv, cv), t, Nat.add(m, cv), Equal.sym(Nat, Nat.add(m, cv), t, ht), hcc)
  +s5 = Equal.trans(Bool, Nat.is_lt(cv, m), Nat.is_lt(Nat.add(cv, cv), Nat.add(m, cv)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(cv, cv), Nat.add(m, cv)), Nat.is_lt(cv, m), WW.lt_cancel_r(cv, m, cv)), s4)
  +s6 = N.lt_trans(lo, cv, m, s3, s5)
  # v mod m = (lo + 1 m) mod m = lo
  %Equal.sym(Nat, v, Nat.add(lo, 1n+mp), e2) : {lo == Nat.mod(_, 1n+mp) : Nat}
  %Equal.sym(Nat, Nat.add(lo, 1n+mp), Nat.add(1n+mp, lo), NA.add_comm(lo, 1n+mp)) : {lo == Nat.mod(_, 1n+mp) : Nat}
  %Equal.sym(Nat, 1n+mp, Nat.mul(1n, 1n+mp), Equal.sym(Nat, Nat.mul(1n, 1n+mp), 1n+mp, SR.one_mul(1n+mp))) : {lo == Nat.mod(Nat.add(_, lo), 1n+mp) : Nat}
  %Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(1n, 1n+mp), lo), 1n+mp), Nat.mod(lo, 1n+mp), NR.absorb(mp, 1n, lo)) : {lo == _ : Nat}
  %Equal.sym(Nat, Nat.mod(lo, 1n+mp), lo, NR.mod_of(0n, mp, lo, s6)) : {lo == _ : Nat}
  {==}

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.is_lt
  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=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend&name=lt_subst_l
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend&name=lt_subst_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend&name=one_mul
  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_trans
  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=add_cancel
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=mod_of
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend&name=lt_cancel_r