proposition: Lemma cardinal_Dyck_NH2 n: #|[set s: (n.+1.*2).-tuple bool | Dyck_NH2 s ]| = catalan n.
proof: Proof. rewrite - cardinal_Dyck_path. symmetry. set T1:= (n.*2).-tuple bool; set T2:= (n.+1.*2).-tuple bool. pose hack (l: seq bool) := take (n.+1.*2) (l ++ (nseq (n.+1.*2.+1) false)). have hack1 l: size l = (n.+1.*2) -> hack l = l. by move => ss; rewrite /hack take_size_cat. have hack2 l: size (hack l) = (n.+1).*2. by rewrite /hack size_take size_cat size_nseq addnS ltnS leq_addl. have ha (x:T1) : size (hack (Dyck_rp x)) == (n.+1.*2). by rewrite hack2. have hb (x:T1): Dyck_path x -> hack(Dyck_rp x) = (Dyck_rp x). by move => h; apply:hack1; rewrite (Dyck_rp_size h) /= size_tuple. pose f l := Tuple (ha l);set lhs := [set s | _]. have aux: {in lhs &, injective (fun x => (Tuple (ha x)))}. move => u v; rewrite !inE => du dv; case; rewrite hb // hb // => eq. by apply/val_inj; rewrite /= -(Dyck_rpK du) -(Dyck_rpK dv) eq. rewrite - (card_in_imset aux); apply:eq_card => x; rewrite !inE. apply/imsetP/idP. by move => [y]; rewrite inE => dy ->; rewrite /= hb //; apply:Dyck_rp_H2. move => h2; move/andP:(h2) => [dpx _]. have sx:size x = n.+1.*2 by rewrite size_tuple. move:(Dyck_lpK h2 sx)=> hh. have dl:=(Dyck_lp_Dyck dpx sx). move:(Dyck_lp_size dpx sx) => /eqP ss. exists (Tuple ss); first by rewrite inE. by apply:val_inj; rewrite /= (Dyck_lpK h2 sx) hack1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)