proposition: Lemma mem_mkPlus : forall r1 r2, mkPlus r1 r2 =i CPlus [:: r1; r2].
proof: Proof. move => r1. case: (toolmkPlus r1). - move => heq r2 u; rewrite (eqP heq) mkPlus_CVoid_lt; clear r1 heq. by rewrite !CPlus_cons -[u \in CPlus _]topredE /= /mem_creg /= orbF. - case => l heq r2 u; rewrite (eqP heq); clear r1 heq. case: (toolmkPlus r2). * move => heq; rewrite (eqP heq) mkPlus_CVoid_rt; clear r2 heq. by rewrite !CPlus_cons -[u \in CPlus _]topredE /= /mem_creg /= orbF. * case => k' heq; rewrite (eqP heq) /mkPlus !CPlus_cons; clear r2 heq. rewrite -[u \in CPlus [::]]topredE /= /mem_creg /= orbF. by rewrite CPlus_mem_match CPlus_cat. * move => h. rewrite toolmkPlus2_r ?CPlus_mem_match1 => //. by rewrite CPlus_cat !CPlus_cons -![u \in CPlus [::]]topredE /= /mem_creg /= orbF. - move => h1 r2 u. case: (toolmkPlus r2). * move => heq; rewrite (eqP heq) mkPlus_CVoid_rt; clear r2 heq. by rewrite !CPlus_cons -[u \in CPlus _]topredE /= /mem_creg /= orbF. * case => k' heq; rewrite (eqP heq) toolmkPlus2_l ?CPlus_mem_match2 => //; clear r2 heq. by rewrite CPlus_cat !CPlus_cons -![u \in CPlus [::]]topredE /= /mem_creg /= !orbF. * move => h. rewrite toolmkPlus3 => //. move: (@compare_eq_axiom r1 r2). case : (compare r1 r2) => //. move => -> //. rewrite !CPlus_cons -![u \in CPlus [::]]topredE /= /mem_creg /= !orbF. by apply/idP/orP; [left | case]. rewrite !CPlus_cons -![u \in CPlus [::]]topredE /= /mem_creg /= !orbF => _. by rewrite orbC. 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)