def nearpm.c0a

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

import Base

862def nearpm.c0a(+a: Nat) -> LE(1n+a, 1n+a):
863  by_contra(1n+a, 1n+a, ng => nearpm.c0a.k(a, ng))

Uses (4)