proposition: Lemma nR_elim : forall l l', (nR l l') <-> (exists2 x: A, InA l x & ~~ InA l' x).
proof: Proof. elim => [ | hd tl ih] /= l'; split => //. by case. case. - move/gpred_list_notinP => hpred. exists hd => //. by apply: InA_hd. - move => hr. case: (ih l') => h _. case: (h hr) => b h1 h2. exists b => //. by case: (eqA_dec b hd) => /=. - case => b. case: (eqA_dec b hd) => /=. move => hbhd _. move/negP => hn. left. apply/gpred_list_notinP. apply/negP. move => h. apply: hn. by rewrite (InA_eq l' hbhd). move => hn_bhd hin hneq. right. apply/ih. by exists b. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)