law lt_w

lawful-bytes@0.1.1.0 · proof_fast_append.bend:317

import Base

317law lt_w:
318  for +w: Nat
319  for +x: Nat
320  for +pp: Nat
321  for +h: {Nat.is_lt(Nat.add(Nat.mul(w, 4n), x), Nat.mul(4n, pp)) == True{} : Bool}
322  {Nat.is_lt(w, pp) == True{} : Bool}