proposition: Lemma neql_dec : forall l1 l2, {neql l1 l2}+{~neql l1 l2}.
proof: Proof. rewrite /neql => x y. case: (nR_dec x y) => h. by left; left. case: (nS_dec x y) => h'. by left; right. right. case => hu. by apply : h. by apply: h'. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)