proposition: Lemma reg_incl_Pr : forall r1 r2 r3, reg_incl r1 r2 -> reg_incl r1 (Plus r3 r2).
proof: Proof. rewrite /reg_incl => r1 r2 r3 h. transitivity (Plus (Plus r1 r3) r2); first by symmetry; apply similar_PlusA. transitivity (Plus (Plus r1 r2) r3); first by apply similar_PlusAC. transitivity (Plus r2 r3) => //. by apply similar_congr_Plus; last reflexivity. Qed.
imports: Coq(RelationClasses Setoid Morphisms Permutation) Coq(SetoidList Mergesort Orders) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp)