proposition: Lemma sumn_diff_shape inner outer : included inner outer -> sumn (outer / inner) = sumn outer - sumn inner.
proof: Proof. elim: inner outer => [// | inn0 inn IHinn] /= [// | out0 out] /=. by rewrite subn0. move/andP => [Hleq Hincl]. rewrite (IHinn _ Hincl) {IHinn}. have Hsumn : sumn inn <= sumn out. elim: inn out Hincl => [// | inn1 inn IHinn] /= [// | out1 out] /=. by move/andP => [H1 /IHinn]; exact: leq_add. by rewrite subnDA (addnBA _ Hsumn) addnC (addnBA _ Hleq) [out0 + _]addnC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype