proposition: Lemma DP_symmetry l: Dyck_path l -> Dyck_path (rev [seq ~~ x | x <- l]).
proof: Proof. move => h. have Ha s: DP_Tcount [seq ~~ x | x <- s] = DP_Fcount s. by elim: s => //a s /= ->; case:a. have Hb s: DP_Fcount [seq ~~ x | x <- s] = DP_Tcount s. by elim: s => //a s /= ->; case:a. move/andP:(h)=> [/eqP ha _]. set s := (rev [seq ~~ x | x <- l]). have bs: DP_balanced s. rewrite /s /DP_balanced - map_rev Ha Hb /DP_Fcount /DP_Tcount !count_rev. by apply/eqP. have hc:forall k, k <= size s -> DP_Tcount (drop k s) >= DP_Fcount (drop k s). move => k kl. rewrite - (cat_take_drop k s) in bs. rewrite (DP_count_sym bs); move: kl; rewrite /s. rewrite -map_rev size_map size_rev - map_take Ha Hb => kl. rewrite (take_rev kl) /DP_Fcount /DP_Tcount !count_rev. by move /andP:(DP_prop2 (size l - k) h) => []. rewrite /Dyck_path bs /=. elim: s hc {ha bs} => // a l' Hr H1 /=; rewrite (H1 0) // andbT. apply: Hr => k kl; exact: (H1 k.+1 kl). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)