proposition: Lemma fset_in_singleton_eq x y : x ∈ {{ y }} ↔ x = y.
proof: Proof. split; intros E. now apply fset_join_singletons_eq_r, join_sl_le_spec, fset_in_singleton_le. rewrite E. apply fset_in_singleton. 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