law sub_zero_sym

bend-mathlib@0.8.1.0 · nat.bend:4004

import Base

4004# Subtracting zero changes nothing: n - 0 = n, reversed to rewrite toward the simple side.
4005law sub_zero_sym:
4006  for n: Nat
4007  {n == Nat.sub(n, 0n) : Nat}