proposition: Lemma card_ord_partitions m n : #|[set t : m.+1.-tuple 'I_n.+1 | \sum_(i <- t) i == n]| = 'C(m + n, m).
proof: Proof. symmetry; set In1 := 'I_n.+1; pose x0 : In1 := ord0. pose f_add (t : m.-tuple In1) := [tuple of sub_ord (\sum_(x <- t) x) :: t]. rewrite -card_partial_ord_partitions -!sum1dep_card (reindex f_add) /=. by apply: eq_bigl => t; rewrite big_cons /= addnC (sameP maxn_idPr eqP) maxnE. exists (fun t : m.+1.-tuple In1 => [tuple of behead t]) => [t _|]. exact: val_inj. case/tupleP=> x t /[!(inE, big_cons)] /eqP def_n. by apply: val_inj; congr (_ :: _); apply: val_inj; rewrite /= -{1}def_n addnK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)