~/jendhub

def rhs.c1b

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

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

404def rhs.c1b(+l: Nat, +a: Nat, +b: Nat, h4: LE(Nat.add(b, a), 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)):
405  by_contra(a, Nat.mul(3n, l), ng => rhs.c1b.k(l, a, b, ng, h4, hs, pl))

Uses (6)

Used by (1)