proposition: Lemma minh_rrw : minh (rot rt (rcons w }})) = - height (take rt w) - 1.
proof: Proof. rewrite -pfminhP pfminh_rrw. rewrite /rot !take_cat !size_drop !size_rcons. rewrite subSn // ltnS ltnn subnn take0 cats0. rewrite height_drop height_simpl /=. move: HDyck => /Dyck_wordP[_ ->]; rewrite add0r addrC. by rewrite -cats1 takel_cat. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree