def le_cancel_r

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/fieldops.bend:200

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

200# m + c = h + h and c <= h: h <= m
201def 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}:
202  %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}
203  %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}
204  NR.le_add_cancel(c, x, y)