proposition: Lemma fset_in_add y X x : y ∈ {{ x }} ⊔ X ↔ y = x ∨ y ∈ X.
proof: Proof. rewrite fset_in_join. split; intros [?|?]; try tauto. left. now apply fset_in_singleton_eq. left. now apply fset_in_singleton_eq. 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