proposition: Lemma ssublPlus2 : forall r1 r2 s, ssubl (Plus r1 r2) s = ssubl r1 s && ssubl r2 s.
proof: Proof. by move => r1 r2 /=. 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)