law w2_bound

lawful-bytes@0.1.1.0 · proof_fast_append.bend:722

import Base

722law w2_bound:
723  for +w: Nat
724  for +pp: Nat
725  for +hp: {Nat.is_lt(0n, pp) == True{} : Bool}
726  for +h: {Nat.is_lt(w, pp) == True{} : Bool}
727  {Nat.is_le(Nat.add(w, 2n), Nat.mul(4n, pp)) == True{} : Bool}