proposition: Lemma neql2n_eql : forall l1 l2, neql l1 l2 -> ~ eql l1 l2.
proof: Proof. move => l1 l2. case/neql_elim => a [|]. - case/andP => h1. move/negP => h2. move/eql_elim => heq. apply: h2. by apply heq. - case/andP. move/negP => h1 h2. move/eql_elim => heq. apply: h1. by apply heq. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)