law sub_self

bend-mathlib@0.8.1.0 · nat.bend:634

import Base

634# A natural minus itself is zero: n - n = 0.
635law sub_self:
636  for n: Nat
637  {Nat.sub(n, n) == 0n : Nat}