law zero_sub

bend-mathlib@0.8.1.0 · nat.bend:622

import Base

622# Truncated subtraction from zero is zero: 0 - n = 0.
623law zero_sub:
624  for n: Nat
625  {Nat.sub(0n, n) == 0n : Nat}