law lt_sub_of

lawful-fields@0.1.1.0 · proof_cut.bend:91

import Base

91# s + r < T gives r < T - s.
92law lt_sub_of:
93  for +s: Nat
94  for +r: Nat
95  for +tt: Nat
96  for +h: {Nat.is_lt(Nat.add(s, r), tt) == True{} : Bool}
97  {Nat.is_lt(r, Nat.sub(tt, s)) == True{} : Bool}