proposition: Lemma l8 n k : (\prod_(0 <= i < k) (n %/ a i) ^ (n %/ a i)) * C n k <= n ^ n.
proof: Proof. pose t := \sum_(0 <= i < k) (n %/ a i). have letn : t <= n by exact: sum_aV_leqn. suff step1 : \prod_(0 <= i < k) (n %/ a i) ^ (n %/ a i) * C n k <= n ^ (n - t) * t ^ t. apply: leq_trans step1 _; case: n t letn => [t | n t leqnSt]. - by rewrite leqn0 => /eqP->. have e : n.+1 = n.+1 - t + t by rewrite subnK. rewrite [in X in _ <= _ ^ X]e {e} expnD leq_mul2l. case: t leqnSt => [| t] leqnSt; first by rewrite !expn0 orbT. by rewrite leq_exp2r // leqnSt orbT. pose l := mkseq (fun i : nat => n %/ a i) k. have lP : 'C[l] * \prod_(0 <= i < k) (n %/ a i) `! = t `!. have -> : \prod_(0 <= i < k) (n %/ a i)`! = \prod_( j <- l) j `! . rewrite [in RHS](big_nth 0) size_mkseq big_nat_cond [RHS]big_nat_cond. apply: eq_bigr => i /andP [/andP [le0i ltik] _]. by rewrite nth_mkseq //. have -> : t = \sum_(j <- l) j. rewrite /t [RHS](big_nth 0) size_mkseq big_nat_cond [RHS]big_nat_cond. apply: eq_bigr => i /andP [/andP [le0i ltik] _] . by rewrite nth_mkseq // . exact: multi_prod_fact. have /eqP -> : C n k == (n ^_ (n - t)) * 'C[l]. have /eqn_pmul2l <- : \prod_(0 <= i < k) (n %/ a i) `! > 0. by apply: prodn_gt0 => i; rewrite fact_gt0. rewrite C_multi mulnA mulnC mulnA lP mulnC. have {2}-> : t = n - (n - t) by rewrite subKn. by rewrite ffact_fact // leq_subr. have -> : \prod_(0 <= i < k) (n %/ a i) ^ (n %/ a i) = \prod_( j <- l) j ^ j. rewrite [in RHS](big_nth 0) size_mkseq big_nat_cond [RHS]big_nat_cond. apply: eq_bigr => i /andP [/andP [le0i ltik] _]. by rewrite nth_mkseq //. have Ht : t = \sum_(i <- l) i. rewrite /t [in RHS](big_nth 0) size_mkseq big_nat_cond [RHS]big_nat_cond. apply: eq_bigr => i /andP [/andP [le0i ltik] _]. by rewrite nth_mkseq //. rewrite mulnC -mulnA. apply: leq_mul. - exact: ffact_le_expn. - by rewrite Ht; apply: multinomial_ineq. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics floor arithmetics multinomial