proposition: Lemma card_sorted_tuples m n : #|[set t : m.-tuple 'I_n.+1 | sorted leq (map val t)]| = 'C(m + n, m).
proof: Proof. set In1 := 'I_n.+1; pose x0 : In1 := ord0. have add_mnP (i : 'I_m) (x : In1) : i + x < m + n. by rewrite -ltnS -addSn -!addnS leq_add. pose add_mn t i := Ordinal (add_mnP i (tnth t i)). pose add_mn_nat (t : m.-tuple In1) i := i + nth x0 t i. have add_mnC t: val \o add_mn t =1 add_mn_nat t \o val. by move=> i; rewrite /= (tnth_nth x0). pose f_add t := [tuple of map (add_mn t) (ord_tuple m)]. rewrite -card_ltn_sorted_tuples -!sum1dep_card (reindex f_add) /=. apply: eq_bigl => t; rewrite -map_comp (eq_map (add_mnC t)) map_comp. rewrite enumT unlock val_ord_enum -[in LHS](drop0 t). have [m0 | m_gt0] := posnP m. by rewrite {2}m0 /= drop_oversize // size_tuple m0. have def_m := subnK m_gt0; rewrite -{2}def_m addn1 /= {1}/add_mn_nat. move: 0 (m - 1) def_m => i k; rewrite -[in RHS](size_tuple t) => def_m. rewrite (drop_nth x0) /=; last by rewrite -def_m leq_addl. elim: k i (nth x0 t i) def_m => [|k IHk] i x /=. by rewrite add0n => ->; rewrite drop_size. rewrite addSnnS => def_m; rewrite -addSn leq_add2l -IHk //. by rewrite (drop_nth x0) // -def_m leq_addl. pose sub_mn (t : m.-tuple 'I_(m + n)) i : In1 := inord (tnth t i - i). exists (fun t => [tuple of map (sub_mn t) (ord_tuple m)]) => [t _ | t]. apply: eq_from_tnth => i; apply: val_inj. by rewrite /sub_mn !(tnth_ord_tuple, tnth_map) addKn inord_val. rewrite inE /= => inc_t; apply: eq_from_tnth => i; apply: val_inj. rewrite tnth_map tnth_ord_tuple /= tnth_map tnth_ord_tuple. suffices [le_i_ti le_ti_ni]: i <= tnth t i /\ tnth t i <= i + n. by rewrite /sub_mn inordK ?subnKC // ltnS leq_subLR. pose y0 := tnth t i; rewrite (tnth_nth y0) -(nth_map _ (val i)) ?size_tuple //. case def_e: (map _ _) => [|x e] /=; first by rewrite nth_nil ?leq_addr. set nth_i := nth (i : nat); rewrite def_e in inc_t; split. have: i < size (x :: e) by rewrite -def_e size_map size_tuple ltn_ord. elim: (val i) => //= j IHj lt_j_e. by apply: leq_trans (pathP (val i) inc_t _ lt_j_e); rewrite ltnS IHj 1?ltnW. move: (_ - _) (subnK (valP i)) => k /=. elim: k (val i) => /= [|k IHk] j; rewrite -ltnS -addSn ?add0n => def_m. by rewrite def_m -def_e /nth_i (nth_map y0) ?ltn_ord // size_tuple -def_m. rewrite (leq_trans _ (IHk _ _)) -1?addSnnS //; apply: (pathP _ inc_t). rewrite -ltnS (leq_trans (leq_addl k _)) // -addSnnS def_m. by rewrite -(size_tuple t) -(size_map val) def_e. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)