law four_lt_e

lawful-bytes@0.1.1.0 · proof_core.bend:498

import Base

498# 4 * 2^d < 2^e for d + 2 < e (e stays a variable here: 2^32 must never be
499# unfolded, so the callers instantiate e = 32n only in the final type).
500law four_lt_e:
501  for +d: Nat
502  for +e: Nat
503  for +he: {Nat.is_lt(Nat.add(2n, d), e) == True{} : Bool}
504  {Nat.is_lt(Nat.mul(4n, Nat.pow(2n, d)), Nat.pow(2n, e)) == True{} : Bool}