proposition: Lemma last_rot_pfminh : last {{ (rot pfminh w) = }}.
proof: Proof. rewrite /rot last_cat -nth_pfminh -nth_last size_takel ?pfminh_size //. rewrite nth_take; last by case: pfminh pfminh_pos. apply: set_nth_default. by case: pfminh pfminh_pos pfminh_size. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree