proposition: Lemma included_anti sh1 sh2 : is_part sh1 -> is_part sh2 -> included sh1 sh2 -> included sh2 sh1 -> sh1 = sh2.
proof: Proof. move=> psh1 psh2 in12 in21; apply included_sumnE => //. by apply anti_leq; rewrite !sumn_included. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype