proposition: Lemma from_parttupleK t (H : is_parttuple t) : parttuple (part_fromtuple H) = t.
proof: Proof. apply eq_from_tnth => i. by rewrite tnth_mktuple sumn_take_part_fromtuple // (tnth_nth 0). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype