def le_add_cancel

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/arith.bend:62

import Base

62# d + x <= d + y is x <= y
63def le_add_cancel(+d: Nat, +x: Nat, +y: Nat) -> {Nat.is_le(Nat.add(d, x), Nat.add(d, y)) == Nat.is_le(x, y) : Bool}:
64  match d:
65    case 0n:
66      {==}
67    case 1n+ +dp:
68      le_add_cancel(dp, x, y)