~/jendhub

def nearhi.c0a

bend-kit-collections@0.1.4.1 · nat_order.bend:812

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

812def nearhi.c0a(+a: Nat, +c: Nat, +c2: Nat, n1: LE(c, 1n+c2)) -> LE(Nat.add(a, c), 1n+Nat.add(a, c2)):
813  by_contra(Nat.add(a, c), 1n+Nat.add(a, c2), ng => nearhi.c0a.k(a, c, c2, ng, n1))

Uses (5)

Used by (1)