proposition: Lemma ssublr_ok : forall a b, (ssubl a b -> {subset a <= b}) /\ (ssubr a b -> {subset b <= a}).
proof: Proof. rewrite /sub_mem. elim => [ | | |s | c hc | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c hc ] //. - move => b; split. + move => _ x. by rewrite -topredE /=. by apply ssubrVoid_ok. - move => b; split. + by apply ssublEps_ok. by apply ssubrEps_ok. - move => b; split. + by apply ssublDot_ok. by apply ssubrDot_ok. - move => b; split. + by apply ssublAtom_ok. by apply ssubrAtom_ok. - have h1 : (forall b, ssubl c b -> forall x, x \in c -> x \in b) by apply hc. have h2 : (forall b, ssubr c b -> forall x, x \in b -> x \in c) by apply hc. clear hc; split. + by apply ssublStar_ok. by apply ssubrStar_ok. - have h1 : (forall b, ssubl c1 b -> forall x, x \in c1 -> x \in b) by apply hc1. have h2 : (forall b, ssubr c1 b -> forall x, x \in b -> x \in c1) by apply hc1. have h3 : (forall b, ssubl c2 b -> forall x, x \in c2 -> x \in b) by apply hc2. have h4 : (forall b, ssubr c2 b -> forall x, x \in b -> x \in c2) by apply hc2. clear hc1 hc2; split. + by apply ssublPlus_ok. by apply ssubrPlus_ok. - have h1 : (forall b, ssubl c1 b -> forall x, x \in c1 -> x \in b) by apply hc1. have h2 : (forall b, ssubr c1 b -> forall x, x \in b -> x \in c1) by apply hc1. have h3 : (forall b, ssubl c2 b -> forall x, x \in c2 -> x \in b) by apply hc2. have h4 : (forall b, ssubr c2 b -> forall x, x \in b -> x \in c2) by apply hc2. clear hc1 hc2; split. + by apply ssublAnd_ok. by apply ssubrAnd_ok. - have h1 : (forall b, ssubl c1 b -> forall x, x \in c1 -> x \in b) by apply hc1. have h2 : (forall b, ssubr c1 b -> forall x, x \in b -> x \in c1) by apply hc1. have h3 : (forall b, ssubl c2 b -> forall x, x \in c2 -> x \in b) by apply hc2. have h4 : (forall b, ssubr c2 b -> forall x, x \in b -> x \in c2) by apply hc2. clear hc1 hc2; split. + by apply ssublConc_ok. by apply ssubrConc_ok. have h1 : (forall b, ssubl c b -> forall x, x \in c -> x \in b) by apply hc. have h2 : (forall b, ssubr c b -> forall x, x \in b -> x \in c) by apply hc. clear hc; split. - by apply ssublNot_ok. by apply ssubrNot_ok. 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)