def pow2_le_pow

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32.bend:58

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as SC

58def pow2_le_pow(+n: Nat, +k: Nat, +hk: {Nat.is_le(k, n) == True{} : Bool}) -> {Nat.is_le(SC.pow2(k), Nat.pow(2n, n)) == True{} : Bool}:
59  %pow2_pow(n) : {Nat.is_le(SC.pow2(k), _) == True{} : Bool}
60  N.pow2_mono(k, n, hk)