proposition: Lemma one_plus_invx_expx (p q : nat) : 0 < p%:Q / q%:Q -> exp_quo (1 + q%:Q / p%:Q) p q <= ratr 9%:Q.
proof: Proof. move=> /ltr_neq. rewrite eq_sym mulf_eq0 invr_eq0 negb_or !intr_eq0 -!lt0n => /andP[Hp Hq]. have [leqp|ltpq] := leqP q p. pose f := (p %/ q)%N. apply: (@le_trans _ _ (ratr 8%:Q)); last by rewrite ler_rat. suff: exp_quo (1 + q%:~R / p%:~R) p q <= exp_quo (1 + f%:Q^-1) f.+1 1. by move=> /le_trans -> //; rewrite -exp_quo_r_nat ler_rat one_plus_invn_expn. rewrite exp_quo_lessE ?addr_ge0 ?mulr_ge0 ?invr_ge0 ?ler0n // muln1. have: (1 + f%:~R^-1)%:C ^+ p <= (1 + f%:~R^-1)%:C ^+ (f.+1 * q). by rewrite exp_incr_expp ?ler1q ?lerDl ?invr_ge0 ?ler0n 1?ltnW ?ltn_ceil. apply: le_trans. rewrite lerXn2r ?nnegrE ?ler0q ?addr_ge0 ?mulr_ge0 ?invr_ge0 ?ler0n //. rewrite ler_rat lerD2l ler_pdivrMr ?ltr0n // mulrC. rewrite ler_pdivlMr ?ltr0n ?divn_gt0 //. by rewrite -intrM ler_nat mulnC leq_trunc_div. pose f := (q %/ p)%N. have Helper0 : (0 < f)%N. by rewrite divn_gt0 // ltnW. have Helper1 : 0 <= 1 + q%:Q / p%:Q. by rewrite addr_ge0 ?divr_ge0 ?ler0n. have Helper2 : 1 + q%:Q / p%:Q <= 1 + (1 + f%:~R). rewrite lerD2l -mulrS ler_pdivrMr ?ltr0n // -natrM ler_nat. by rewrite ltnW ?ltn_ceil. have Helper3 : (p * f <= q)%N. by rewrite mulnC leq_trunc_div. apply: (@le_trans _ _ (exp_quo (1 + (1 + f%:Q)) p q)). by apply: exp_quo_less; rewrite // !addr_ge0 ?ler0n. apply: (@le_trans _ _ (exp_quo (1 + (1 + f%:Q)) 1 f)). by apply: exp_quo_lessn; rewrite //= ?lerDl ?addr_ge0 ?ler0n // mul1n. apply: (@le_trans _ _ (exp_quo ((3 ^ f.+1)%N%:Q) 1 f)). rewrite exp_quo_less // ?addr_ge0 ?ler0n //. by rewrite -rat1 -!natrD ler_nat !add1n replace_exponential. rewrite /exp_quo expr1 !CratrE expnS natrM rootCMr ?ler0n //. have -> : 9%:R = 3%:R * 3%:R :> algC by rewrite -natrM. by rewrite ler_pM ?root_le_x ?rootC_ge0 ?ler0n ?natrX // ler_eXnr ?ler1n. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) extra_mathcomp posnum hanson_elem_arith