proposition: Lemma fset_meet_singletons_eq_l x y : {{ x }} ⊓ {{ y }} = {{ x }} ↔ x = y.
proof: Proof. split; intros E. apply fset_in_singleton_eq. rewrite fset_eq_in in E. setoid_rewrite fset_in_meet in E. now destruct (proj2 (E x) (fset_in_singleton _)). now rewrite E, fset_meet_singletons. 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