proposition: Lemma ssubrNot_ok : forall a, (forall b, ssubl a b -> forall x, x \in a -> x \in b) -> forall b, ssubr (Not a) b -> forall x, x \in b -> x \in (Not a).
proof: Proof. move => a ha. elim => [ | | |t | d _ | d1 hd1 d2 hd2 | d1 _ d2 _ | d1 _ d2 _ | d _ ] //. - by rewrite ssubrPlus2; case/andP => h1 h2 x; rewrite -topredE /=; case/orP => hx ; [rewrite (hd1 h1 x hx) | rewrite (hd2 h2 x hx)]. rewrite ssubrNot => h x. rewrite -topredE /= /compl /=; move/negP=> h1. rewrite -topredE /= /compl /=. apply/negP => hn. apply: h1. by apply (ha d h x hn). 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)