proposition: Lemma listset_to_list_preserves_join l k : listset_to_list (l ⊔ k) = listset_to_list l ⊔ listset_to_list k.
proof: Proof. destruct l as [l Pl], k as [k Pk]. unfold join, listset_join, listset_join_raw. simpl. clear Pk Pl. induction l; simpl; intros; [easy|]. now rewrite <-IHl, listset_add_raw_cons. 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