proposition: Lemma remark_7_3 : let f := fun u => exp_quo (u / (a i)%:Q) in f n%:Q n (a i) / ((n %/ a i) ^ (n %/ a i))%N%:Q%:C <= f n%:Q n (a i) / f (n.+1 - a i)%N%:Q (n.+1 - a i)%N (a i).
proof: Proof. rewrite /= ler_pdivrMr; last first. by rewrite ltr0q ltr0n expn_gt0 divn_gt0 ?Hain. rewrite[X in _ <= X]mulrC mulrA ler_pdivlMr. - rewrite mulrC; apply/ler_wpM2l/remark_7_2. by apply: exp_quo_ge0; rewrite // divr_ge0 ?ler0n. - by apply: exp_quo_gt0; rewrite // divr_gt0 // ltr0n ?subn_gt0. Qed.
imports: ZArith mathcomp(all_ssreflect all_algebra all_field) extra_mathcomp tactics binomialz floor arithmetics posnum rat_of_Z hanson_elem_arith hanson_elem_analysis