~/jendhub

def almhi.c0a

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

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

746def almhi.c0a(+wl: Nat, +wh: Nat, +w2: Nat, o1: LE(wh, Nat.mul(3n, wl)), n2: LE(w2, 1n+wh)) -> LE(w2, Nat.add(3n, Nat.mul(3n, wl))):
747  by_contra(w2, Nat.add(3n, Nat.mul(3n, wl)), ng => almhi.c0a.k(wl, wh, w2, ng, o1, n2))

Uses (6)

Used by (1)