proposition: Lemma ssublPlus_ok : forall a c, (forall b, ssubl a b -> forall x, x \in a -> x \in b) -> (forall d, ssubl c d -> forall x, x \in c -> x \in d) -> forall r, ssubl (Plus a c) r -> forall x, x \in (Plus a c) -> x \in r.
proof: Proof. move => a c ha hc r. rewrite ssublPlus2; case/andP => h1 h2 x. by rewrite -topredE /=; case/orP => hu; [ apply (ha r h1 x hu) | apply (hc r h2 x hu) ]. 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)