proposition: Lemma ribbon_sumn_diffE inner outer : is_part outer -> ribbon inner outer -> (sumn (outer / inner)).-1.+1 = (sumn (outer / inner)).
proof: Proof. move=> partout Hrib. have:= ribbon_sumn_lt partout Hrib; rewrite -subn_gt0. rewrite -(sumn_diff_shape (ribbon_included Hrib)). by case: sumn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition