law lt_add_mono_r

lawful-words@0.1.0.0 · proof_nat.bend:882

import lawful-words@0.1.0.0/proof_nat.bend as ProofNat
import Base

882law lt_add_mono_r:
883  for +c: Nat
884  for +a: Nat
885  for +b: Nat
886  for h: {Nat.is_lt(a, b) == True{} : Bool}
887  {Nat.is_lt(Nat.add(a, c), Nat.add(b, c)) == True{} : Bool}

Uses (6)

Used by (1)