~/jendhub

def rls.c0a

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

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

273def rls.c0a(+l: Nat, +a: Nat, +b: Nat, h4: LE(Nat.add(a, b), Nat.add(3n, Nat.mul(3n, l))), hs: LE(1n+a, Nat.mul(2n, b)), pl: LE(1n, l)) -> LE(a, Nat.mul(3n, l)):
274  by_contra(a, Nat.mul(3n, l), ng => rls.c0a.k(l, a, b, ng, h4, hs, pl))

Uses (6)

Used by (1)