law sub_mono
import lawful-fields@0.1.1.0/proof_num.bend as ProofNumimport 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}