proposition: Lemma lreg_incl1 : forall r l, reg_incl r (rPlus r l).
proof: Proof. rewrite /reg_incl => r. elim => [ | hd tl hi] //=. transitivity (Plus (Plus r (rPlus r tl)) hd). - by symmetry; apply similar_PlusA. 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)