proposition: Lemma ssubrPlus2 : forall r1 r2 s, ssubr s (Plus r1 r2) = ssubr s r1 && ssubr s r2.
proof: Proof. move => r1 r2. by case. Qed.
imports: Coq(RelationClasses Setoid Morphisms Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(regexp finite_der equiv)