proposition: Lemma Dyck_of_balK w : height w = 0 -> w = bal_of_Dyck (pfminh (rcons w }})) (Dyck_of_bal w).
proof: Proof. move=> Hbal; apply val_inj => /=. have -> : size w = (size (rcons w }})).-1 by rewrite size_rcons. rewrite (@rot_pfminhE (rcons w }})); last by rewrite height_simpl /= Hbal add0r. rewrite rotK size_take size_rot size_rcons /= ltnSn. by rewrite -cats1 take_size_cat. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree