proposition: Lemma ssublNot_ok : forall a, (forall b, ssubr a b -> forall x, x \in b -> x \in a) -> forall b, ssubl (Not a) b -> forall x, x \in (Not a) -> x \in b.
proof: Proof. move => a ha. elim => [ | | |t | d _ | d1 hd1 d2 hd2 | d1 _ d2 _ | d1 _ d2 _ | d _ ] //. - by rewrite ssublPlus1 => //; case/orP => hu x hx; rewrite -topredE /=; apply/orP; [left; rewrite (hd1 hu x hx) | right; rewrite (hd2 hu x hx)]. rewrite ssublNot => 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)