proposition: Lemma remark_7_2 : exp_quo ((n.+1 - a i)%N%:Q / (a i)%:Q) (n.+1 - a i) (a i) <= ((n %/ a i) ^ (n %/ a i))%N%:Q%:C.
proof: Proof. rewrite exp_quo_nat_nat; apply: exp_quo_self_grows => //. - by rewrite divr1. - by rewrite divr_gt0 // ltr0n subn_gt0. - by rewrite ler1n divn_gt0. by rewrite ler_pdivrMr // -natrM ler_nat remark_7_1. 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