proposition: Lemma l7 n i (Hain : (a i <= n)%N) : exp_quo (n%:Q / (a i)%:Q) n (a i) / ((n %/ a i) ^ (n %/ a i))%N%:Q%:C < exp_quo (10%N%:Q * n%:Q / (a i)%:Q) (a i - 1) (a i).
proof: Proof. have posai_rat : 0 < (a i)%:Q by rewrite ltr0n. pose posai := PosNumDef posai_rat. have -> : (a i)%:Q = num_of_pos posai by []. have lt0n : (0 < n)%N by exact: leq_trans Hain. have lt0n_rat : 0 < n%:Q by rewrite ltr0n. pose posn := PosNumDef lt0n_rat. have -> : n%:Q = num_of_pos posn by []. apply: le_lt_trans (remark_7_3 Hain) _. set lhs := (X in X < _); set rhs := (X in _ < X). suff : lhs ^+ a i < rhs ^+ a i. rewrite ltr_pXn2r // nnegrE; last exact: exp_quo_ge0. by rewrite /lhs divr_ge0 // exp_quo_ge0 // divr_ge0 // ler0z. rewrite remark_7_4 // /rhs -mulrA ![_ ^+ _ ^+ a i]exprAC !rootCK //. rewrite rmorphD rmorphXn 15!(rmorph1, rmorph_int, rmorphM, fmorphV) /=. rewrite [(10%:~R * _) ^+ _]exprMn ltr_pM2r ?exprn_gt0 ?divr_gt0 ?ltr0n //. set x := (n.+1 - a i)%N. set y := (a i - 1)%N. rewrite -root_lt_x ?exprn_ge0 ?addr_ge0 ?divr_ge0 ?ler0n ?subn_gt0 //. have: 9%:~R < 10%:~R :> algC by rewrite ltr_nat. have/one_plus_invx_expx: 0 < x%:~R / y%:~R :> rat. by rewrite divr_gt0 // ltr0n subn_gt0. rewrite /exp_quo rmorphD rmorphM fmorphV !rmorph1 !rmorph_int. by rewrite rootCX ?addr_ge0 ?divr_ge0 ?ler0n ?subn_gt0 //; exact: le_lt_trans. 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