proposition: Lemma intpartn2 (sh : 'P_2) : sh = rowpartn 2 \/ sh = colpartn 2.
proof: Proof. by case: (val_intpartn2 sh) => sheq; [left | right]; apply val_inj; rewrite /= {}sheq ?rowpartnE ?colpartnE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype