law pow_le

lawful-words@0.1.0.0 · proof_nat.bend:1438

import Base

1438# 2^m <= 2^k for m <= k.
1439law pow_le:
1440  for +m: Nat
1441  for +k: Nat
1442  for +h: {Nat.is_le(m, k) == True{} : Bool}
1443  {Nat.is_le(Nat.pow(2n, m), Nat.pow(2n, k)) == True{} : Bool}