law pow_pos

lawful-words@0.1.0.0 · proof_nat.bend:1391

import Base

1391law pow_pos:
1392  for +k: Nat
1393  {Nat.is_lt(0n, Nat.pow(2n, k)) == True{} : Bool}