proposition: Lemma parttupleP sh : is_parttuple (parttuple sh).
proof: Proof. apply/is_parttupleP; split. - by rewrite tnth_mktuple /= take0. - by rewrite tnth_mktuple take_intpartn_over // sumn_intpartn. - apply/(sortedP 0) => i; rewrite size_tuple => ltid. rewrite !nth_parttuple //; last exact: ltnW. case: (ltnP i (size sh)) => Hi. by rewrite (take_nth 0) // sumn_rcons leq_addr. by rewrite !take_oversize // (leq_trans Hi). - move=> [|i]// /andP[_ ltid]. rewrite !nth_parttuple /= ?ltnS //=; try exact: ltnW; first last. by apply ltnW; apply ltnW. rewrite -addnn !sumn_take !big_nat_recr //= -!addnA leq_add2l. rewrite [X in _ <= X]addnC addnA leq_add2l. by have /is_partP[_] : is_part sh by []. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype