proposition: Lemma mkPlusC : forall r1 r2, mkPlus r1 r2 = mkPlus r2 r1.
proof: Proof. move => r1 r2. case: (toolmkPlus r1). - by move => heq; rewrite (eqP heq) mkPlus_CVoid_lt mkPlus_CVoid_rt. - case => l heq; rewrite (eqP heq). case: (toolmkPlus r2). + by move => heq2; rewrite (eqP heq2) mkPlus_CVoid_lt mkPlus_CVoid_rt. + case => l' heq2; rewrite (eqP heq2) /mkPlus. rewrite /merge' merge_sort_sym => //. by apply: leS_trans. by apply : leS_antisym. by apply: leS_total. apply: sort_sorted. by apply: leS_total. apply: sort_sorted. by apply: leS_total. + move => h; rewrite toolmkPlus2_r ?toolmkPlus2_l => //. rewrite /merge' merge_sort_sym => //. by apply: leS_trans. by apply : leS_antisym. by apply: leS_total. apply: sort_sorted. by apply: leS_total. - move => h. case: (toolmkPlus r2). + by move => heq; rewrite (eqP heq) mkPlus_CVoid_lt mkPlus_CVoid_rt. + case => l heq; rewrite (eqP heq) toolmkPlus2_l ?toolmkPlus2_r => //. rewrite /merge' merge_sort_sym => //. by apply: leS_trans. by apply : leS_antisym. by apply: leS_total. apply: sort_sorted. by apply: leS_total. + move => h'. rewrite toolmkPlus3 ?toolmkPlus3 => //. rewrite compare_neg. move: (@compare_eq_axiom r2 r1). case: (compare r2 r1) => //=. by move => ->. 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)