proposition: Lemma parttupleK sh : from_parttuple (parttuple sh) = sh.
proof: Proof. have /andP[/eqP Hsum Hpart] := from_parttupleP (parttupleP sh). apply: sumn_take_inj => // k. case: (ltnP k d.+1) => [ltkd1 | /ltnW ltdk]. have /= -> := sumn_take_part_fromtuple (parttupleP sh) ltkd1. by rewrite (nth_map ord0) ?size_enum_ord // nth_enum_ord. rewrite take_intpartn_over //. rewrite !take_oversize ?Hsum /= -?{1}(sumn_intpartn sh) //. by apply: (leq_trans _ ltdk); rewrite -Hsum size_part. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype