law sub_self

lawful-bytes@0.1.1.0 · proof_shift.bend:105

import Base

105law sub_self:
106  for +j: Nat
107  {Nat.sub(j, j) == 0n : Nat}