proposition: Lemma ssublrD : forall r , ssubl r (Dot char) = ssubr (Dot char) r.
proof: Proof. elim => [ | | | a | c hc | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c hc ] //. by rewrite ssublPlus2 ssubrPlus2 hc1 hc2. 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)