def almhi.w0
bend-kit-collections@0.1.4.1 · nat_order.bend:767
import bend-kit-collections@0.1.4.1/nat_order.bend as NatOrder
import Base
import bend-mathlib@0.7.4.0/bool.bend as MBool
767def almhi.w0(+wl: Nat, +wh: Nat, +w2: Nat, +o1: LE(wh, Nat.mul(3n, wl)), +o2: LE(wl, Nat.mul(3n, wh)), +n1: LE(wh, 1n+w2), +n2: LE(w2, 1n+wh)) -> {alm(wl, w2) == True{} : Bool}:
768 MBool.and_eq_true(Nat.is_le(w2, Nat.add(3n, Nat.mul(3n, wl))), Nat.is_le(wl, Nat.add(3n, Nat.mul(3n, w2))), almhi.c0a(wl, wh, w2, o1, n2), almhi.c0b(wl, wh, w2, o2, n1))