proposition: Lemma fset_notin_empty x : x ∉ ∅.
proof: Proof. intro. now apply fset_singleton_ne_empty with x, below_bottom, fset_in_singleton_le. Qed.
imports: MathClasses.theory.lattices MathClasses.varieties.monoids MathClasses.implementations.bool MathClasses.implementations.list_finite_set MathClasses.orders.lattices MathClasses.interfaces.abstract_algebra MathClasses.interfaces.finite_sets MathClasses.interfaces.orders