proposition: Lemma listset_add_raw_NoDupA (l : list A) (x : A) : NoDupA (=) l → NoDupA (=) (listset_add_raw x l).
proof: Proof. intros Pl. induction l; simpl. now apply NoDupA_singleton. case (decide_rel _); intros E1; auto. inversion_clear Pl. apply NoDupA_cons; auto. intros E2. destruct (listset_add_raw_InA _ _ _ E2); intuition. 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