proposition: Lemma UDn_Dyck : tval UDn \is a Dyck_word.
proof: Proof. rewrite /=; apply/Dyck_wordP; rewrite height_take_leq; split => [i|]. - rewrite (eqP size_UDn). elim: n i => //= m IHm [|[|i]] //. rewrite doubleS ltnS ltnS !height_simpl /= addrA subrr add0r. exact: IHm. - by elim: n => //= m; rewrite !height_simpl /= addrA subrr add0r. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree