proposition: Lemma fset_singleton_ne_empty x : {{ x }} ≠ ∅.
proof: Proof. intros E1. set (g (z : A) := true). assert (Setoid_Morphism g) by (split; try apply _; firstorder). assert (fset_extend g {{ x }} ≠ ⊥) as E2. rewrite <-(fset_extend_correct_applied g). discriminate. destruct E2. now rewrite E1, preserves_bottom. 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