law sub_self_sym

bend-mathlib@0.8.1.0 · nat.bend:4020

import Base

4020# A natural minus itself is zero: n - n = 0, reversed to rewrite toward the simple side.
4021law sub_self_sym:
4022  for n: Nat
4023  {0n == Nat.sub(n, n) : Nat}