law succ_ne_zero

bend-mathlib@0.8.1.0 · nat.bend:168

import Base

168# A successor is not zero.
169law succ_ne_zero:
170  for -n: Nat
171  {1n+n != 0n : Nat}