law le_add_mono_l

lawful-words@0.1.0.0 · proof_nat.bend:856

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

856law le_add_mono_l:
857  for +c: Nat
858  for +a: Nat
859  for +b: Nat
860  for h: {Nat.is_le(a, b) == True{} : Bool}
861  {Nat.is_le(Nat.add(c, a), Nat.add(c, b)) == True{} : Bool}

Uses (4)

Used by (16)