proposition: Lemma pfminh_rrw : pfminh (rot rt (rcons w }})) = ((size w).+1 - rt)%N.
proof: Proof. apply/esym/pfminhE => [|i|i]. - by rewrite size_rot size_rcons subSn // ltnS leq_subr. - rewrite /rot !take_cat !size_drop !size_rcons. rewrite subSn // ltnS ltnn subnn take0 cats0 ltnS. rewrite -(leq_add2r rt) subnK //. case: leqP => Hi. + rewrite take_drop !height_drop take_takel ?leq_addl //. rewrite lerBDr subrK -cats1 takel_cat //. rewrite !height_simpl /= addr0. move: HDyck => /Dyck_wordP[H1 ->]. rewrite add0r; apply: (le_trans _ (H1 _)). by rewrite -oppr_ge0 opprK. + rewrite height_simpl addrC -lerBlDr subrr. case: (leqP (i - (size w - rt).+1) rt) => [H | /ltnW H]. * rewrite take_takel // -cats1 takel_cat; last exact: leq_trans H Hrt. by move: HDyck => /Dyck_wordP[->]. * rewrite take_oversize ?size_take ?size_rcons ?ltnS ?Hrt //. rewrite -cats1 takel_cat //. by move: HDyck => /Dyck_wordP[->]. - rewrite subSn // ltnS => Hi. rewrite /rot !take_cat !size_drop !size_rcons. rewrite subSn // ltnS ltnn subnn take0 cats0 ltnS Hi. rewrite take_drop !height_drop take_takel ?leq_addl //. rewrite ltrBlDl addrC subrK. rewrite height_rcons /=; move: HDyck => /Dyck_wordP[_ ->]. move: Hi; rewrite -(leq_add2r rt) subnK // => Hi. rewrite add0r -cats1 takel_cat //. rewrite -subr_gt0 opprK ltzD1. by move: HDyck => /Dyck_wordP[H1 _]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree