law sub_le_of

lawful-fields@0.1.1.0 · proof_cut.bend:74

import Base

74# T <= s + r gives T - s <= r.
75law sub_le_of:
76  for +tt: Nat
77  for +s: Nat
78  for +r: Nat
79  for +h: {Nat.is_le(tt, Nat.add(s, r)) == True{} : Bool}
80  {Nat.is_le(Nat.sub(tt, s), r) == True{} : Bool}