def sub_self

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/nat.bend:290

import Base

290def sub_self(+n: Nat) -> {Nat.sub(n, n) == 0n : Nat}:
291  match n:
292    case 0n:
293      {==}
294    case 1n+p:
295      sub_self(p)