proposition: Lemma cardinal_swap_but_last n: #|[set X:{set 'I_(n.*2.+2) } | #|X| ==n ]| = #|[set X:{set 'I_(n.*2.+2)} | (#|X| == n.+1) && ~~Dyck_path (char_seq X) ]|.
proof: Proof. pose T := {set 'I_(n.*2.+2) }. pose f (x:T):T := list_to_set (n.*2.+2) (Dyck_modify (char_seq x)). have Ha (x:T): size (Dyck_modify (char_seq x)) = (n.*2.+2). by rewrite Dyck_modify_size size_char_seq. have Hb: involutive f. by move=> x;rewrite /f (list_to_setK (Ha x)) Dyck_modify_inv set_to_listK. rewrite !card_set_pred -(card_imset _ (inv_inj Hb));apply: eq_card => x. rewrite !inE; apply/imsetP/idP => [ [y yp ->] | /andP[ca cb]]. rewrite /f set_to_list_cardinal (list_to_setK (Ha y)). set l := char_seq y. move: yp; rewrite inE set_to_list_cardinal -/l => /eqP tt. have /eqP tt2: DP_Fcount l == n.+2. by rewrite - (DP_count' (m:=n)) ? tt// /l size_char_seq - addnn - 2!addnS. have w3: DP_pos l = false. move:tt tt2; clear;case: l => // a l /= -> ->. by rewrite leqNgt /= leqnSn andbF. move:tt2; rewrite - tt; move/Dyck_modify_tcount_bis. move /andP => [-> _]; rewrite /Dyck_path DP_splita_pos1. move:(Dyck_modify_split l) => /andP[/eqP -> _]. by rewrite swap_but_last_nil - DP_splita_pos1 w3 andbF. exists (f x); last by rewrite Hb. move: ca; rewrite set_to_list_cardinal => tt. rewrite inE set_to_list_cardinal /f (list_to_setK (Ha x)). set l := char_seq x. have sc: DP_balanced l. rewrite /DP_balanced eq_sym. by rewrite - (DP_count' (m:=n.+1)) // size_char_seq (eqP tt) addnn. have sd:~~ nilp (DP_splita l).1. by rewrite - DP_splita_pos1; move: cb; rewrite /Dyck_path sc. by move/andP:(Dyck_modify_tcount sc sd) =>[]; rewrite (eqP tt) eqSS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)