def nearpm.c0b

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

import Base

872def nearpm.c0b(+a: Nat) -> LE(a, 1n+1n+a):
873  by_contra(a, 1n+1n+a, ng => nearpm.c0b.k(a, ng))

Uses (4)