proposition: Lemma ribbon_sumn_lt inner outer : is_part outer -> ribbon inner outer -> sumn inner < sumn outer.
proof: Proof. move=> partout Hrib; rewrite ltnNge; apply/negP=> lesz. have incl := ribbon_included Hrib. have eqsum : sumn inner = sumn outer. by apply anti_leq; rewrite (sumn_included incl) lesz. by have := ribbon_noneq Hrib; rewrite (included_sumnE partout incl) // eqxx. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition