proposition: Lemma delta_asympt : {large : nat | forall n, (large <= n)%N -> ((a n)%:CR * z3 - (b n)%:CR <= (Kdelta * (1 / a n))%:CR)%CR}.
proof: Proof. pose_big_enough large. exists large => n hlarge. apply: (@lecr_trans _ (6%:Q%:CR * z3 * (1 / a n)%:CR))%CR; last first. rewrite cst_crealM. by apply/lecr_mulf2r/divr_ge0/le_0_a; first exact: le_ubound. rewrite {1}z3_eq_b_over_a; apply: (@le_crealP _ n) => i leni /=. rewrite mul1r lerBlDr mulrC -ler_pdivlMr ?lt_0_a // mulrDl. rewrite -[_ / _ / _]mulrA -[_ / _]invfM -expr2 -lerBlDr. rewrite -/(b_over_a_seq n). have leSnSi : (n.+1 <= i.+1)%N by []. rewrite z3seqE mulr_sumr (big_cat_nat _ _ _ _ leSnSi) //= mulrDl ler_wpDl //. rewrite divr_ge0 ?exprn_ge0 ?le_0_a ?sumr_ge0 // => k _. by rewrite divr_ge0 ?exprn_ge0 ?ler0n. rewrite big_add1 /= Db_over_a_casoratian; [ | raise_big_enough | exact: leni]. rewrite mulr_suml; apply: ler_sum_nat => j /andP[hnj hji]. rewrite -mulrSr ler_pM2l; last by apply/divr_gt0/exprz_gt0; rewrite ltr0n. rewrite lef_pV2; [| apply/mulr_gt0; exact: lt_0_a..]. by apply: ler_pM; rewrite ?le_0_a //; apply: a_incr; lia. by close. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp(bigenough cauchyreals) extra_mathcomp extra_cauchyreals tactics shift bigopz arithmetics seq_defs c_props s_props z3seq_props a_props b_props b_over_a_props