proposition: Lemma Dyck_cut_ex D : D != [Dyck of [::]] -> exists i, (i != 0)%N && (height (take i D) == 0).
proof: Proof. move=> Hnnil; have:= DyckP D => /Dyck_wordP[_ Heq]. exists (size D); apply/andP; split; first by case: D Hnnil {Heq} => [[]]. - by rewrite take_size Heq. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree