def internal_succ_ne_zero

bend-mathlib@0.8.1.0 · nat.bend:164

import Base

164def internal_succ_ne_zero(-n: Nat, e: {1n+n == 0n : Nat}) -> Empty:
165  %e : Bool.pick(Type, Nat.is_eq(_, 0n), Empty, Unit)
166  Unit{}