law pos_add_l

lawful-words@0.1.0.0 · proof_nat.bend:828

import Base

828law pos_add_l:
829  for +x: Nat
830  for +y: Nat
831  for h: {Nat.is_lt(0n, x) == True{} : Bool}
832  {Nat.is_lt(0n, Nat.add(x, y)) == True{} : Bool}