proposition: Lemma nS_dec : forall x y, {nS x y} + { ~ nS x y}.
proof: Proof. move => x y. elim: (nR_dec y x) => h. by left. by right. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)