proposition: Lemma listset_in_meet_raw l k x : x ∈ l ⊓ k ↔ x ∈ l ∧ x ∈ k.
proof: Proof. unfold meet, contains, listset_in_raw. split. intros E; split; revert E. induction l; simpl. intuition. case (decide_rel); intros ? E; intuition. inversion_clear E; intuition. induction l; simpl. intros E1; inversion E1. case (decide_rel); intros ? E1; intuition. inversion_clear E1 as [?? E2|]; auto. now rewrite E2. intros [E1 E2]. induction l; simpl; [easy|]. case (decide_rel); intros E3. inversion_clear E1; intuition. inversion_clear E1 as [?? E4|]; intuition. destruct E3. now rewrite <-E4. 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