law lt_w0

lawful-bytes@0.1.1.0 · proof_fast_append.bend:686

import Base

686law lt_w0:
687  for +w: Nat
688  for +pp: Nat
689  for +h: {Nat.is_lt(Nat.mul(w, 4n), Nat.mul(4n, pp)) == True{} : Bool}
690  {Nat.is_lt(w, pp) == True{} : Bool}