proposition: Lemma mkAndC : forall r1 r2, mkAnd r1 r2 = mkAnd r2 r1.
proof: Proof. move => r1 r2. case: (toolmkAnd r1). - move => heq; by rewrite (eqP heq) mkAnd_CVoid_lt mkAnd_CVoid_rt. - move => heq; by rewrite (eqP heq) mkAnd_CAll_lt mkAnd_CAll_rt. - case => l heq; rewrite (eqP heq). case: (toolmkAnd r2). + by move => heq2; rewrite (eqP heq2) mkAnd_CVoid_lt mkAnd_CVoid_rt. + by move => heq2; rewrite (eqP heq2) mkAnd_CAll_lt mkAnd_CAll_rt. + case => l' heq2; rewrite (eqP heq2). rewrite /mkAnd. 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 toolmkAnd2_r ?toolmkAnd2_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: (toolmkAnd r2). + by move => heq; rewrite (eqP heq) mkAnd_CVoid_lt mkAnd_CVoid_rt. + by move => heq2; rewrite (eqP heq2) mkAnd_CAll_lt mkAnd_CAll_rt. + case => l heq; rewrite (eqP heq). rewrite toolmkAnd2_l ?toolmkAnd2_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 toolmkAnd3 ?toolmkAnd3 => //. 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)