proposition: Lemma card_ltn_sorted_tuples m n : #|[set t : m.-tuple 'I_n | sorted ltn (map val t)]| = 'C(n, m).
proof: Proof. have [-> | n_gt0] := posnP n; last pose i0 := Ordinal n_gt0. case: m => [|m]; last by apply: eq_card0; case/tupleP=> [[]]. by apply: (@eq_card1 _ [tuple]) => t; rewrite [t]tuple0 inE. rewrite -[n in RHS]card_ord -card_draws. pose f_t (t : m.-tuple 'I_n) := [set i in t]. pose f_A (A : {set 'I_n}) := [tuple of mkseq (nth i0 (enum A)) m]. have val_fA (A : {set 'I_n}) : #|A| = m -> val (f_A A) = enum A. by move=> Am; rewrite -[enum _](mkseq_nth i0) -cardE Am. have inc_A (A : {set 'I_n}) : sorted ltn (map val (enum A)). rewrite -[enum _](eq_filter (mem_enum _)). rewrite -(eq_filter (mem_map val_inj _)) -filter_map. by rewrite (sorted_filter ltn_trans) // unlock val_ord_enum iota_ltn_sorted. rewrite -!sum1dep_card (reindex_onto f_t f_A) /= => [|A]; last first. by move/eqP=> cardAm; apply/setP=> x; rewrite inE -(mem_enum A) -val_fA. apply: eq_bigl => t. apply/idP/idP => [inc_t|/andP [/eqP t_m /eqP <-]]; last by rewrite val_fA. have ft_m: #|f_t t| = m. rewrite cardsE (card_uniqP _) ?size_tuple // -(map_inj_uniq val_inj). exact: (sorted_uniq ltn_trans ltnn). rewrite ft_m eqxx -val_eqE val_fA // -(inj_eq (inj_map val_inj)) /=. apply/eqP/(irr_sorted_eq ltn_trans ltnn) => // y. by apply/mapP/mapP=> [] [x t_x ->]; exists x; rewrite // mem_enum inE in t_x *. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)