law pow_lt

lawful-arrays@0.1.0.0 · proof_base.bend:272

import Base

272law pow_lt:
273  for +d: Nat
274  for +e: Nat
275  for h: {Nat.is_lt(d, e) == True{} : Bool}
276  {Nat.is_lt(Nat.pow(2n, d), Nat.pow(2n, e)) == True{} : Bool}