not singleton

Stream: Is there code for X?

[Alex Kontorovich]

Does something like this already exist? (To say that a type has at least two distinct elements?)

structure NotSingleton (α : Type _) : Prop where
  not_singleton : ∃ x y : α, x ≠ y

[Jireh Loreaux]

docs#Nontrivial