proposition: Lemma mkPlusAC: forall r1 r2 r3, wf_re r1 -> wf_re r2 -> wf_re r3 -> mkPlus (mkPlus r1 r2) r3 = mkPlus (mkPlus r1 r3) r2.
proof: Proof. move => r1 r2 r3. case: (toolmkPlus r1). - move => heq; rewrite (eqP heq); clear heq r1. rewrite !mkPlus_CVoid_lt. by rewrite mkPlusC. - case => l1 heq; rewrite (eqP heq); clear heq r1. move => hw1. case: (toolmkPlus r2). + move => heq; rewrite (eqP heq); clear heq r2. by rewrite !mkPlus_CVoid_rt. + case => l2 heq; rewrite (eqP heq); clear heq r2. move => hw2. case : (toolmkPlus r3). * move => heq; rewrite (eqP heq); clear heq r3. by rewrite !mkPlus_CVoid_rt. * case => l3 heq ; rewrite (eqP heq) => hw3 ; clear heq r3. by rewrite mkPlusAC_plus_plus_plus. * move => hh1 hw3. by rewrite mkPlusAC_plus_plus_nplus. + move => hh1 hw2. case: (toolmkPlus r3). * move => heq; rewrite (eqP heq); clear heq r3. by rewrite !mkPlus_CVoid_rt. * case => l3 heq ; rewrite (eqP heq) => hw3 ; clear heq r3. by rewrite mkPlusAC_plus_plus_nplus. move => hh2 hw3. rewrite !(mkPlusC (CPlus l1) _ ). rewrite -!mkPlusAC_nplus_nplus_plus => //. by rewrite (mkPlusC r2 r3). - move => hh1 hw1. case: (toolmkPlus r2). + move => heq; rewrite (eqP heq); clear heq r2. by rewrite !mkPlus_CVoid_rt. + case => l2 heq; rewrite (eqP heq) => hw2; clear heq r2. case : (toolmkPlus r3). * move => heq; rewrite (eqP heq); clear heq r3. by rewrite !mkPlus_CVoid_rt. * case => l3 heq ; rewrite (eqP heq) => hw3 ; clear heq r3. rewrite !(mkPlusC r1). rewrite -!mkPlusAC_plus_plus_nplus => //. by rewrite (mkPlusC (CPlus l2) (CPlus l3)). * move => hh3 hw3. by rewrite mkPlusAC_nplus_nplus_plus. + move => hh2 hw2. case: (toolmkPlus r3). * move => heq; rewrite (eqP heq); clear heq r3. by rewrite !mkPlus_CVoid_rt. * case => l3 heq ; rewrite (eqP heq) => hw3 ; clear heq r3. by rewrite mkPlusAC_nplus_nplus_plus. * move => hh3 hw3. by rewrite mkPlusAC_nplus_nplus_nplus. 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)