law fits_e

lawful-bytes@0.1.1.0 · proof_core.bend:512

import Base

512law fits_e:
513  for +x: Nat
514  for +d: Nat
515  for +e: Nat
516  for +he: {Nat.is_lt(Nat.add(2n, d), e) == True{} : Bool}
517  for +hx: {Nat.is_le(x, Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
518  {Nat.is_lt(x, Nat.pow(2n, e)) == True{} : Bool}