Reduce.canon0_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 193-198 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=193&end_line=198

import Base
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/ineq.bend as I

# v + cv = lo < t = m + cv: v < m, and v mod m = v
def canon0_val(+mp: Nat, +v: Nat, +cv: Nat, +lo: Nat, +t: Nat, +ht: {Nat.add(1n+mp, cv) == t : Nat}, +ll: {Nat.is_lt(lo, t) == True{} : Bool}, +eu: {Nat.add(v, cv) == lo : Nat}) -> {v == Nat.mod(v, 1n+mp) : Nat}:
  +s1 = I.lt_subst_l(lo, Nat.add(v, cv), t, Equal.sym(Nat, Nat.add(v, cv), lo, eu), ll)
  +s2 = I.lt_subst_r(Nat.add(v, cv), t, Nat.add(1n+mp, cv), Equal.sym(Nat, Nat.add(1n+mp, cv), t, ht), s1)
  +s3 = Equal.trans(Bool, Nat.is_lt(v, 1n+mp), Nat.is_lt(Nat.add(v, cv), Nat.add(1n+mp, cv)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(v, cv), Nat.add(1n+mp, cv)), Nat.is_lt(v, 1n+mp), WW.lt_cancel_r(v, 1n+mp, cv)), s2)
  Equal.sym(Nat, Nat.mod(v, 1n+mp), v, NR.mod_of(0n, mp, v, s3))

Uses (11):
  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_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  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/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