proposition: Lemma UnDn_Dyck : tval UnDn \is a Dyck_word.
proof: Proof. apply/Dyck_wordP; rewrite height_take_leq; split => [i|]. - rewrite (eqP size_UnDn) take_cat !size_nseq => Hi2. case: leqP => [Hi | /ltnW Hi {Hi2}]. + rewrite height_simpl take_nseq /=; last by rewrite leq_subLR addnn. by rewrite !height_nseq mulrN1 mulr1 subr_ge0 lez_nat leq_subLR addnn. + by rewrite take_nseq // height_nseq /= mulr1 lez_nat. - by rewrite height_cat !height_nseq /= mulrN1 mulr1 subrr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree