def wok_r

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

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

16def wok_r(+wl: Nat, +wh: Nat, e: {wok(wl, wh) == True{} : Bool})
17  -> {Nat.is_le(wl, mul3(wh)) == True{} : Bool}:
18  MBool.eq_true_of_and_right(Nat.is_le(wh, mul3(wl)), Nat.is_le(wl, mul3(wh)), e)