proposition: Lemma wf_CPlus_nplus_nplus : forall r1 r2, wf_re r1 -> wf_re r2 -> (r1 != CVoid /\ (forall l, r1 != CPlus l)) -> (r2 != CVoid /\ (forall l, r2 != CPlus l)) -> wf_re (mkPlus r1 r2).
proof: Proof. move => r1 r2 hw1 hw2 hh1 hh2. rewrite toolmkPlus3 => //. case_eq (compare r1 r2) => heq //=. - apply/andP; split => //. rewrite andbT. apply/negP. rewrite mem_seq1 => heq2. by rewrite (eqP heq2) compare_refl in heq. apply/andP; split. rewrite andbT. by rewrite /cregexp_le /leS /cmpS /= heq. by rewrite hw1 hw2. - apply/andP; split. rewrite andbT. apply/negP. rewrite mem_seq1 => heq2. by rewrite (eqP heq2) compare_refl in heq. move : heq. rewrite compare_neg /cregexp_le /leS /cmpS /=. case: (compare r2 r1) => //=. by rewrite hw1 hw2. Qed.
imports: Coq(RelationClasses Setoid Morphisms) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue regexp finite_der equiv)