proposition: Lemma n_neql2eql : forall l1 l2, ~ neql l1 l2 -> eql l1 l2.
proof: Proof. move => l1 l2 hneq. apply/eql_elim => x; split => h. - case_eq (InA l2 x) => heq2 //=. case: hneq. apply/neql_elim. exists x; left. apply/andP ; split => //. by rewrite heq2. - case_eq (InA l1 x) => heq1 //=. case: hneq. apply/neql_elim. exists x; right. apply/andP ; split => //. by rewrite heq1. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)