proposition: Lemma included_sumnE inner outer : is_part outer -> included inner outer -> sumn inner = sumn outer -> inner = outer.
proof: Proof. elim: inner outer => [| inn0 inn IHinn] /=. by move=> outer Houter _ /esym/(part0 Houter) ->. case=> [// | outer0 out] /= /andP[_ {}/IHinn Hrec] /andP[H0 Hincl] Heq. by have:= leq_addE H0 (sumn_included Hincl) Heq => [] [-> /(Hrec Hincl) ->]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype