proposition: Lemma ssubl_r : forall r, (forall s, ssubl r s = ssubr s r) /\ (forall s, ssubl s r = ssubr r s).
proof: Proof. elim => [ | | | a | c hc | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c hc ]. - split. + by move => s; rewrite !ssublVoid !ssubrVoid. by move => s; apply ssublrV. - split. + elim => // r1 hr1 r0 hr0. by rewrite ssublPlus1 // ssubrPlus1 // hr1 hr0. by move => s; apply ssublrE. - split. + elim => // r1 hr1 r0 hr0. by rewrite ssublPlus1 // ssubrPlus1 // hr1 hr0. by move => s; apply ssublrD. - split. + elim => //. * move => b /=. by rewrite eq_sym. move => r1 hr1 r0 hr0. by rewrite ssublPlus1 // ssubrPlus1 // hr1 hr0. by move => s; apply ssublrA. - case: hc => hc1 hc2. split. + elim => //. * move => r h; by rewrite ssublStar ssubrStar (hc1 r). move => r1 hr1 r2 hr2. by rewrite ssublPlus1 // ssubrPlus1 // hr1 hr2. elim => //. + move => r h; by rewrite ssublStar ssubrStar (hc2 r). move => r1 hr1 r2 hr2. by rewrite ssublPlus2 ssubrPlus2 hr1 hr2. - split; case: hc1 hc2 => hc11 hc12 [hc21 hc22]. + move => s. by rewrite ssublPlus2 ssubrPlus2 (hc11 s) (hc21 s). elim => [ | | | t | c' _ | c1' hc1' c2' hc2' | c1' _ c2' _ | c1' _ c2' _ | c' _ ] ; try (by rewrite ssublPlus1 // ssubrPlus1 // hc12 hc22). by rewrite ssublPlus2 ssubrPlus2 hc1' hc2'. - case: hc1 hc2 => hc11 hc12 [hc21 hc22]; split. + elim => //. * move => r1 hr1 r2 hr2. by rewrite ssublPlus1 // ssubrPlus1 // hr1 hr2. move => r1 hr1 r2 hr2. by rewrite ssublAnd ssubrAnd (hc11 r1) (hc21 r2). elim => //. + move => r1 h1 r2 h2. by rewrite ssublPlus2 ssubrPlus2 h1 h2. move => r1 hr1 r2 hr2. by rewrite ssublAnd ssubrAnd hc12 hc22. - case: hc1 hc2 => hc11 hc12 [hc21 hc22]; split. + elim => //. * move => r1 hr1 r2 hr2. by rewrite ssublPlus1 // ssubrPlus1 // hr1 hr2. move => r1 hr1 r2 hr2. by rewrite ssublConc ssubrConc (hc11 r1) (hc21 r2). elim => //. + move => r1 h1 r2 h2. by rewrite ssublPlus2 ssubrPlus2 h1 h2. move => r1 hr1 r2 hr2. by rewrite ssublConc ssubrConc hc12 hc22. case: hc => hc1 hc2; split. - elim => //. + move => r1 hr1 r2 hr2. by rewrite ssublPlus1 //ssubrPlus1 // hr1 hr2. move => r hr. by rewrite ssublNot ssubrNot hc2. elim => //. - move => r1 hr1 r2 hr2. by rewrite ssublPlus2 ssubrPlus2 hr1 hr2. move => r hr. by rewrite ssublNot ssubrNot hc1. 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)