proposition: Lemma card_partial_ord_partitions m n : #|[set t : m.-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 add_mn (i j : In1) : In1 := inord (i + j). pose f_add (t : m.-tuple In1) := [tuple of scanl add_mn x0 t]. rewrite -card_sorted_tuples -!sum1dep_card (reindex f_add) /=. apply: eq_bigl => t; rewrite -[\sum_(i <- t) i]add0n. transitivity (path leq x0 (map val (f_add t))) => /=; first by case: map. rewrite -{1 2}[0]/(val x0); elim: {t}(val t) (x0) => /= [|x t IHt] s. by rewrite big_nil addn0 -ltnS ltn_ord. rewrite big_cons addnA IHt /= val_insubd ltnS. have [_ | ltn_n_sx] := leqP (s + x) n; first by rewrite leq_addr. rewrite -(leq_add2r x) leqNgt (leq_trans (valP x)) //=. by rewrite leqNgt (leq_trans ltn_n_sx) ?leq_addr. pose sub_mn (i j : In1) := Ordinal (leq_ltn_trans (leq_subr i j) (valP j)). exists (fun t : m.-tuple In1 => [tuple of pairmap sub_mn x0 t]) => /= t inc_t. apply: val_inj => /=; have{inc_t}: path leq x0 (map val (f_add t)). by move: inc_t; rewrite inE /=; case: map. rewrite [map _ _]/=; elim: {t}(val t) (x0) => //= x t IHt s. case/andP=> le_s_sx /IHt->; congr (_ :: _); apply: val_inj => /=. move: le_s_sx; rewrite val_insubd. case le_sx_n: (_ < n.+1); first by rewrite addKn. by case: (val s) le_sx_n; rewrite ?ltn_ord. apply: val_inj => /=; have{inc_t}: path leq x0 (map val t). by move: inc_t; rewrite inE /=; case: map. elim: {t}(val t) (x0) => //= x t IHt s /andP[le_s_sx inc_t]. suffices ->: add_mn s (sub_mn s x) = x by rewrite IHt. by apply: val_inj; rewrite /add_mn /= subnKC ?inord_val. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)