def le_cancel_l

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/rconst.bend:71

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR

71def le_cancel_l(+c: Nat, +x: Nat, +y: Nat, +h: {Nat.is_le(Nat.add(c, x), Nat.add(c, y)) == True{} : Bool}) -> {Nat.is_le(x, y) == True{} : Bool}:
72  Equal.trans(Bool, Nat.is_le(x, y), Nat.is_le(Nat.add(c, x), Nat.add(c, y)), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(c, x), Nat.add(c, y)), Nat.is_le(x, y), NR.le_add_cancel(c, x, y)), h)