Scalarops.le_cancel_r: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarops.bend as Scalarops
Lines 172-176 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarops.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarops.bend&start_line=172&end_line=176

import Base
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

# m + c = h + h and c <= h: h <= m
def le_cancel_r(+x: Nat, +y: Nat, +c: Nat) -> {Nat.is_le(Nat.add(x, c), Nat.add(y, c)) == Nat.is_le(x, y) : Bool}:
  %Equal.sym(Nat, Nat.add(x, c), Nat.add(c, x), NA.add_comm(x, c)) : {Nat.is_le(_, Nat.add(y, c)) == Nat.is_le(x, y) : Bool}
  %Equal.sym(Nat, Nat.add(y, c), Nat.add(c, y), NA.add_comm(y, c)) : {Nat.is_le(Nat.add(c, x), _) == Nat.is_le(x, y) : Bool}
  NR.le_add_cancel(c, x, y)

Uses (7):
  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=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_le
  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/math/natural/arith.bend&name=le_add_cancel