proposition: Lemma Dyck_wordP w : reflect ((forall n, height (take n w) >= 0) /\ (height w = 0)) (w \is a Dyck_word).
proof: Proof. rewrite unfold_in. by apply (iffP andP) => /= [] [H1 /eqP H2]; split => //; apply/Dyck_prefixP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree