proposition: Lemma fset_in_join X Y x : x ∈ X ⊔ Y ↔ x ∈ X ∨ x ∈ Y.
proof: Proof. rewrite <-!to_listset_preserves_in, preserves_join. apply listset_in_join. 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