law sub_sub

lawful-fields@0.1.1.0 · proof_cut.bend:125

import lawful-fields@0.1.1.0/proof_cut.bend as ProofCut

import Base

125law sub_sub:
126  for +tt: Nat
127  for +s: Nat
128  for +k: Nat
129  {Nat.sub(Nat.sub(tt, s), k) == Nat.sub(tt, Nat.add(s, k)) : Nat}

Uses (3)

Used by (1)

lawful-fields@0.1.1.0/proof_cut:slice_drop