proposition: Lemma listset_in_join l k x : x ∈ l ⊔ k ↔ x ∈ l ∨ x ∈ k.
proof: Proof. unfold contains, listset_in_raw, listset_in. rewrite listset_to_list_preserves_join. now apply InA_app_iff. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList MathClasses.implementations.list MathClasses.interfaces.abstract_algebra MathClasses.interfaces.finite_sets MathClasses.interfaces.orders MathClasses.theory.lattices MathClasses.orders.lattices