proposition: Lemma n_eql2neql : forall l1 l2, ~eql l1 l2 -> neql l1 l2.
proof: Proof. move => l1 l2 hneq. case: (neql_dec l1 l2) => h //. case: hneq. by apply: n_neql2eql. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)