proposition: Lemma preim_Dyck_of_balE D : tval D \is a Dyck_word -> (bal_hsz n) :&: (Dyck_of_bal @^-1: [set D]) = [ set bal_of_Dyck (nat_of_ord rt) D | rt : 'I_((size D).+1) & nth {{ (rcons D }}) (size D - rt) == }} ].
proof: Proof. move=> HD; apply/setP => /= u; rewrite !inE. apply/andP/imsetP => /= [[/eqP ubal /eqP Huw] | [v /=]]. - have := Dyck_of_balK ubal; rewrite Huw => ->. have := pfminh_size (rcons u }}). rewrite size_rcons size_tuple -{2}(size_tuple D). rewrite leq_eqVlt => /orP[/eqP ->| Hpfminh]. + exists (Ordinal (ltn0Sn (size D))). * by rewrite inE /= subn0 nth_rcons ltnn eq_refl. * apply val_inj => /=. by rewrite -(size_rcons D }}) /rotr subnn subn0 rot0 rot_size. + exists (Ordinal (Hpfminh)); last by []. rewrite inE /=. have := Dyck_of_balK ubal; rewrite Huw. move=> /(congr1 val)/=; rewrite /rotr/rot. rewrite take_cat size_drop subKn ?size_rcons //; last exact: ltnW. rewrite ltnNge -ltnS Hpfminh /= take_takel ?subSn //. move/(congr1 height)/esym; rewrite ubal height_simpl height_drop. rewrite (take_nth {{) ?size_rcons ?ltnS ?leq_subr //. rewrite !height_simpl /= opprD [(- _ + _)%R]addrC. move: (height (take _ _)) => H; rewrite !addrA subrK {H}. move: HD => /Dyck_wordP[_ ->]; rewrite add0r. by case: (nth _ _ _). - rewrite inE => /eqP Hnth -> {u}; split. + rewrite bal_of_DyckP //; first by case: v {Hnth}. by move: HD => /Dyck_wordP[]. + by apply/eqP/bal_of_DyckK => //; case: v {Hnth}. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree