proposition: Lemma val_intpartn3 (sh : 'P_3) : [\/ sh = [:: 3] :> seq nat, sh = [:: 2; 1] :> seq nat | sh = [:: 1; 1; 1] :> seq nat].
proof: Proof. case: sh => sh Hsh /=; move: Hsh; rewrite enum_partnP. by rewrite /enum_partn /= !inE => /or3P[] /eqP ->; [apply Or31 | apply Or32 | apply Or33]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype