proposition: Lemma is_part_of_add_ribbon : is_part_of_n (nbox.+1 + sumn sh) res.
proof: Proof. by rewrite /is_part_of_n /= sumn_add_ribbon eqxx is_part_add_ribbon. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition