~/jendhub

def nearlo.c0b

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

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

795def nearlo.c0b(+a: Nat, +a2: Nat, +c: Nat, n2: LE(a2, 1n+a)) -> LE(Nat.add(a2, c), 1n+Nat.add(a, c)):
796  by_contra(Nat.add(a2, c), 1n+Nat.add(a, c), ng => nearlo.c0b.k(a, a2, c, ng, n2))

Uses (5)

Used by (1)