law zero_sub_sym

bend-mathlib@0.8.1.0 · nat.bend:4012

import Base

4012# Truncated subtraction from zero is zero: 0 - n = 0, reversed to rewrite toward the simple side.
4013law zero_sub_sym:
4014  for n: Nat
4015  {0n == Nat.sub(0n, n) : Nat}