proposition: Lemma fset_meet_distinct_singletons (x y: A) : x ≠ y → {{ x }} ⊓ {{ y }} = ∅.
proof: Proof. intros E1. apply fset_eq_in. intros z. rewrite fset_in_meet. split. intros [E2 E3]. destruct E1. apply fset_in_singleton_eq in E2. apply fset_in_singleton_eq in E3. now rewrite <-E2, <-E3. intro. now destruct (fset_notin_empty z). 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