law sub_zero

bend-mathlib@0.8.1.0 · nat.bend:610

import Base

610# Subtracting zero changes nothing: n - 0 = n.
611law sub_zero:
612  for n: Nat
613  {Nat.sub(n, 0n) == n : Nat}