def neargt.c0a

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

import Base

885def neargt.c0a(+a: Nat) -> LE(Nat.add(a, 1n), 1n+a):
886  by_contra(Nat.add(a, 1n), 1n+a, ng => neargt.c0a.k(a, ng))

Uses (5)