def pow2_pos

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/nat.bend:440

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC

440def pow2_pos(+k: Nat) -> {Nat.is_le(1n, SC.pow2(k)) == True{} : Bool}:
441  match k:
442    case 0n:
443      {==}
444    case 1n+p:
445      le_trans(1n, SC.pow2(p), Nat.double(SC.pow2(p)), pow2_pos(p), double_self_le(SC.pow2(p)))