proposition: Lemma rPlus2_cat : forall l1 l2 a1 a2 E, similar (Plus (rPlus2 (Conc a1 E) E l1) (rPlus2 (Conc a2 E) E l2)) (rPlus2 (Conc a2 E) E (a1::l1++l2)).
proof: Proof. rewrite /rPlus2. elim => [ | hd tl hi] l2 a1 a2 E //=. transitivity (Plus (Plus (rPlus (Conc a1 E) (map (fun x => Conc x E) tl)) (rPlus (Conc a2 E ) (map (fun x => Conc x E) l2))) (Conc hd E)); first (by apply: similar_PlusAC). transitivity (Plus (rPlus (Conc a2 E) (map (fun x => Conc x E) (a1:: tl ++ l2))) (Conc hd E)) => /=. - apply similar_congr_Plus; last by reflexivity. by apply hi. symmetry; by apply similar_PlusAC. 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)