def internal_zero_ne_succ

bend-mathlib@0.8.1.0 · nat.bend:152

import Base

152def internal_zero_ne_succ(-n: Nat, e: {0n == 1n+n : Nat}) -> Empty:
153  %e : Bool.pick(Type, Nat.is_eq(_, 0n), Unit, Empty)
154  Unit{}