law sub_sub

lawful-bytes@0.1.1.0 · proof_fast_find.bend:322

import Base

322law sub_sub:
323  for +tt: Nat
324  for +s: Nat
325  for +l: Nat
326  {Nat.sub(Nat.sub(tt, s), l) == Nat.sub(tt, Nat.add(s, l)) : Nat}