def neargt.c0b

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

import Base

895def neargt.c0b(+a: Nat) -> LE(a, 1n+Nat.add(a, 1n)):
896  by_contra(a, 1n+Nat.add(a, 1n), ng => neargt.c0b.k(a, ng))

Uses (5)