fact: Fixpoint listset_add_raw (x : A) (l : list A) : list A := match l with | [] => [x] | y :: l => y :: if decide_rel (=) x y then l else listset_add_raw x l end.
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