law c4

lawful-bytes@0.1.1.0 · proof_fast_append.bend:711

import Base

711law c4:
712  for +o: Nat
713  for +y: Nat
714  for +np: Nat
715  for +h: {Nat.is_lt(Nat.add(o, Nat.add(4n, y)), Nat.add(np, 4n)) == True{} : Bool}
716  {Nat.is_lt(Nat.add(o, y), np) == True{} : Bool}