proposition: Lemma ssublrA : forall r u, ssubl r (Atom u) = ssubr (Atom u) r.
proof: Proof. elim => [ | | | a | c hc | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c hc ] // u. - by rewrite /= eq_sym. 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)