def lt_add_cancel

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natfuel.bend:481

import Base

481def lt_add_cancel(+d: Nat, +x: Nat, +y: Nat) -> {Nat.is_lt(Nat.add(d, x), Nat.add(d, y)) == Nat.is_lt(x, y) : Bool}:
482  match d:
483    case 0n:
484      {==}
485    case 1n+ +e:
486      lt_add_cancel(e, x, y)