def nearhi.c0b

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

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

import Base

826def nearhi.c0b(+a: Nat, +c: Nat, +c2: Nat, n2: LE(c2, 1n+c)) -> LE(Nat.add(a, c2), 1n+Nat.add(a, c)):
827  by_contra(Nat.add(a, c2), 1n+Nat.add(a, c), ng => nearhi.c0b.k(a, c, c2, ng, n2))

Uses (5)

Used by (1)

bend-kit-collections@0.1.4.1/nat_order:nearhi.w0