law sub_mono

lawful-fields@0.1.1.0 · proof_cut.bend:107

import Base

107law sub_mono:
108  for +a: Nat
109  for +b: Nat
110  for +c: Nat
111  for +h: {Nat.is_le(a, b) == True{} : Bool}
112  {Nat.is_le(Nat.sub(a, c), Nat.sub(b, c)) == True{} : Bool}