proposition: Lemma rot_pfminhE : rcons (take (size w).-1 (rot pfminh w)) }} = rot pfminh w.
proof: Proof. rewrite -{2}(cat_take_drop (size w).-1 (rot pfminh w)). suff -> : drop (size w).-1 (rot pfminh w) = [:: }}] by rewrite cats1. have hsz : size (drop (size w).-1 (rot pfminh w)) = 1%N. rewrite size_drop size_rot /=. by case: w Hbal1 => //= w0 tlw _; rewrite subSn // subnn. apply (eq_from_nth (x0 := {{)) => [// | n]. rewrite hsz ltnS leqn0 => /eqP ->. rewrite nth_drop addn0 /= -(size_rot pfminh) nth_last. exact: last_rot_pfminh. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree