proposition: Lemma Dyck_prefixP w : reflect (forall n, height (take n w) >= 0) (w \is a Dyck_prefix).
proof: Proof. rewrite unfold_in; apply (iffP allP) => /= H. - by move=> i; apply H; apply take_prefixes. - by move=> p /mem_prefixesP[i ->{p}]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree