proposition: Lemma card_preim_Dyck_of_bal D : tval D \is a Dyck_word -> #|(bal_hsz n) :&: (Dyck_of_bal @^-1: [set D])| = n.+1.
proof: Proof. move=> HD. rewrite (preim_Dyck_of_balE HD). rewrite card_in_imset; first last. move=> [i Hi] [j Hj]; rewrite !inE /= => /eqP Hnthi /eqP Hnthj Heq. wlog ilt : i j Hi Hj Hnthi Hnthj Heq / (i <= j)%N. move=> ileqj; case: (leqP i j); first exact: ileqj. by move=> /ltnW/ileqj ->. apply val_inj => /=; move: Hi Hj; rewrite !ltnS => Hi Hj. move: Heq => /(congr1 (fun x => rcons (val x) }})). rewrite !rcons_bal_of_Dyck // /rotr => /(congr1 pfminh). case: i Hi Hnthi ilt => [|i] //=; rewrite ?subn0. - move=> _ Hnth _; case: j Hj Hnthj => // j Hj Hnthj. rewrite rot_size -{1}(rot0 (rcons D }})). rewrite !pfminh_rrw //= size_rcons; last by rewrite subSS leq_subr. rewrite subn0 subKn ?ltnS; last exact: ltnW. by move=> [] Heq; move: Hj; rewrite Heq ltnn. - case: j Hj Hnthj => // j Hj Hnthj Hi Hnthi. rewrite ltnS => Hij. rewrite !pfminh_rrw //= size_rcons ?subSS ?leq_subr //. rewrite !subSn ?leq_subr //. by rewrite !subKn ?ltnS; try exact: ltnW. rewrite -(card_imset _ rev_ord_inj). have -> : n.+1 = count_mem }} (rcons D }}). rewrite count_rcons /= addn1 count_mem_height0 //. by move: HD => /Dyck_wordP[]. rewrite -(@card_preim_nth (size D).+1 _ _ _ {{); last by rewrite size_rcons. congr (#|pred_of_set _|). apply/setP => /= i; apply/imsetP/idP => /= [[j] |]. - rewrite inE => /eqP Hnthj ->{i} /=. by rewrite inE /= subSS Hnthj. - rewrite inE => Hnth. exists (rev_ord i); last by rewrite rev_ordK. by rewrite inE /= subSS subKn // -ltnS. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree