def nearrf.c0a

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

import Base

839def nearrf.c0a(+a: Nat) -> LE(a, 1n+a):
840  by_contra(a, 1n+a, ng => nearrf.c0a.k(a, ng))

Uses (4)