~/jendhub

def sub_self

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

import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as Nat
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)

Uses (2)

Used by (14)