~/jendhub

def almhi.c0b

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

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

764def almhi.c0b(+wl: Nat, +wh: Nat, +w2: Nat, o2: LE(wl, Nat.mul(3n, wh)), n1: LE(wh, 1n+w2)) -> LE(wl, Nat.add(3n, Nat.mul(3n, w2))):
765  by_contra(wl, Nat.add(3n, Nat.mul(3n, w2)), ng => almhi.c0b.k(wl, wh, w2, ng, o2, n1))

Uses (6)

Used by (1)