proposition: Lemma nR_dec : forall x y, {nR x y} +{~ nR x y}.
proof: Proof. rewrite /nR. elim => [ | hd tl ih] /= y. by right. case: (ih y) => [heq | hneq]. by left; right. case_eq (InA y hd) => h. right. case. by apply/gpred_list_notinP. by apply : hneq. left. left. apply/gpred_list_notinP. by rewrite h. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)