proposition: Lemma neqs_perm : forall l l' k k', Permutation l l' -> Permutation k k' -> neql l k -> neql l' k'.
proof: Proof. move => l l' k k' hP1 hP2. case/neql_elim => a [ | ]. - case/andP => h1 h2. apply/neql_elim; exists a; left; apply/andP ; split. apply/InA2P. apply Permutation_InA2 with l => //. by apply/InA2P. move/negP: h2 => h2. apply/negP => h3. apply : h2. apply/InA2P. apply Permutation_InA2 with k'. by symmetry. by apply/InA2P. - case/andP => h1 h2. apply/neql_elim; exists a; right; apply/andP ; split. move/negP: h1 => h1. apply/negP => h3. apply : h1. apply/InA2P. apply Permutation_InA2 with l'. by symmetry. by apply/InA2P. apply/InA2P. apply Permutation_InA2 with k => //. by apply/InA2P. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)