def lt_cancel_l

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/width.bend:271

import Base

271def lt_cancel_l(+d: Nat, +x: Nat, +y: Nat) -> {Nat.is_lt(Nat.add(d, x), Nat.add(d, y)) == Nat.is_lt(x, y) : Bool}:
272  match d:
273    case 0n:
274      {==}
275    case 1n+ +e:
276      lt_cancel_l(e, x, y)