proposition: Lemma one_plus_invn_expn (n : nat) : (1 + n%:Q^-1) ^+ n.+1 <= 8%:Q.
proof: Proof. case: n => // n. have step: (1 + n.+1%:Q^-1) ^+ n.+1 <= \sum_(i < n.+2) i`!%:Q^-1. rewrite exprDn; apply: ler_sum => i _; rewrite expr1n mul1r -mulr_natr exprVn. rewrite ler_pdivrMl ?ler_pdivlMr ?ltr0n ?expn_gt0 ?fact_gt0 //. by rewrite -natrM bin_ffact -natrX ler_nat ffact_le_expn. have {step}: (1 + n.+1%:Q^-1) ^+ n.+2 <= 2%:Q * \sum_(i < n.+2) i`!%:Q^-1. rewrite exprS; apply: ler_pM => //. by rewrite -[2%:Q]/(1 + 1) lerD2l invf_le1 // ler1z. move/le_trans; apply; rewrite -[8%:Q]/(2%:Q * 4%:Q) ler_pM2l //. have: 1 + \sum_(i < n.+1) (2%:Q / 3%:Q) ^+ i <= 4%:Q. rewrite geometric_sum // -[4%:Q]/(1 + 3%:Q) lerD2l. have -> : 1 - 2%:Q / 3%:Q = 3%:Q^-1 by []. by rewrite invrK ler_piMl // lerBlDr lerDl. apply: le_trans; rewrite big_ord_recl lerD2l; apply: ler_sum => i _ /=. by rewrite -invf_div exprVn lef_pV2 ?posrE ?ltr0n ?fact_gt0 ?fact_greater_geom. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) extra_mathcomp posnum hanson_elem_arith