law sub_mono

lawful-fields@0.1.1.0 · proof_num.bend:176

import lawful-fields@0.1.1.0/proof_num.bend as ProofNum
import Base

176law sub_mono:
177  for +a: Nat
178  for +b: Nat
179  for +c: Nat
180  for +h: {Nat.is_le(a, b) == True{} : Bool}
181  {Nat.is_le(Nat.sub(a, c), Nat.sub(b, c)) == True{} : Bool}

Uses (7)

Used by (1)