proposition: Lemma tool_converse : forall S, r_incl S (r_union (r_inter S (r_not nR)) nR).
proof: Proof. rewrite /r_union. move => S x y hxy. case: (nR_dec x y) => [heq | hneq]. by right. left. by split. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)