proposition: Lemma ssublPlusl : forall r s t, ssubl r s -> ssubl r (Plus s t).
proof: Proof. move => r s t. elim : r => [ | | | u | c hc | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c hc ] //; try (by rewrite ssublPlus1 // => ->). rewrite ssublPlus2. case/andP => h1 h2 /=; by rewrite 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)