def AP.lt_cancel

bend-osdev-array@0.1.0.1 · PROOF.bend:63

import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF

import Base

63def AP.lt_cancel(s: Nat, -r: Nat, -u: Nat) -> {Nat.is_lt(Nat.add(s, r), Nat.add(s, u)) == Nat.is_lt(r, u) : Bool}:
64  match s:
65    case 0n:
66      {==}
67    case 1n+q:
68      AP.lt_cancel(q, r, u)

Uses (4)

Used by (3)