proposition: Lemma Dyck_of_balP w : height w = 0 -> tval (Dyck_of_bal w) \is a Dyck_word.
proof: Proof. rewrite /Dyck_of_bal /= => Hw. rewrite -[size w]/(size w).+1.-1 -(size_rcons w }}). by apply rot_is_Dyck; rewrite height_simpl /= Hw add0r. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree