def wok_l

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

import Base
import bend-mathlib@0.7.4.0/bool.bend as MBool

12def wok_l(+wl: Nat, +wh: Nat, e: {wok(wl, wh) == True{} : Bool})
13  -> {Nat.is_le(wh, mul3(wl)) == True{} : Bool}:
14  MBool.eq_true_of_and_left(Nat.is_le(wh, mul3(wl)), Nat.is_le(wl, mul3(wh)), e)