proposition: Lemma nS_nR_In : forall l l', nS l l' <-> nR l' l.
proof: Proof. done. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)