law zero_ne_succ

bend-mathlib@0.8.1.0 · nat.bend:156

import Base

156# Zero is not a successor.
157law zero_ne_succ:
158  for -n: Nat
159  {0n != 1n+n : Nat}