~/jendhub

def nearrf.c0b

bend-kit-collections@0.1.4.1 · nat_order.bend:849

import bend-kit-collections@0.1.4.1/nat_order.bend as NatOrder
import Base

849def nearrf.c0b(+a: Nat) -> LE(a, 1n+a):
850  by_contra(a, 1n+a, ng => nearrf.c0b.k(a, ng))

Uses (4)

Used by (1)