proposition: Lemma z3seq_b_over_a_asympt : {asympt e : i / `|z3seq i - b_over_a_seq i| < e}.
proof: Proof. exists_big_modulus M rat. move=> eps i peps hmi /=. suff step1 : \sum_(0 <= i0 < Posz i + 1 :> int) `|c i i0 * s i i0| < eps * a i. suff -> : b_over_a_seq i = z3seq i + (\sum_(0 <= k < Posz i + 1 :> int) c i k * s i k) / a i. rewrite opprD addNKr normrN normrM normfV. rewrite [X in _ / X](gtr0_norm (lt_0_a _)) // ltr_pdivrMr ?lt_0_a //. exact: le_lt_trans (ler_norm_sum _ _ _) _. apply: canLR (mulfK _) _; rewrite ?mulrDl ?divfK ?a_neq0 //. rewrite mulr_sumr -big_split /=; apply: eq_bigr => j _. by rewrite /v /u mulrDr mulrC. rewrite -PoszD !eq_big_int_nat /=. have step2 (i0 : nat) : (0 <= i0 <= i)%N -> `|c i i0 * s i i0| <= c i i0 * i0%:Q / (2%:Q * i%:Q ^ 2). case/andP=> _ hi0; rewrite normrM [`|c i i0|]gtr0_norm ?lt_0_c //. rewrite -mulrA ler_pM2l //; last exact: lt_0_c. apply: s_maj; rewrite // ltr0n; raise_big_enough. apply: (@le_lt_trans _ _ (\sum_(0 <= i0 < i + 1) c i i0 * i0%:Q / (2%:Q * i%:Q ^ 2))). apply: ler_sum_nat => j /andP[h0j]. rewrite addn1 ltnS => hji; exact: step2. apply:(@le_lt_trans _ _ ((\sum_(0 <= i0 < i + 1) c i i0) / (2%:Q * i%:Q))). rewrite mulr_suml; apply: ler_sum_nat => j /andP[h0j]. rewrite addn1 ltnS => hji; rewrite -mulrA ler_pM2l ?lt_0_c //. rewrite mulrA invfM mulrCA ger_pMr; last by rewrite gtr0E mulr_gt0 ?ltr0n. by rewrite ler_pdivrMr ?ltr0n // mul1r ler_nat. rewrite mulrC -eq_big_int_nat /= ltr_pM2r; last first. rewrite -/(a i); exact: lt_0_a. rewrite invfM ltr_pdivrMr ?ltr0n // mulrC -ltr_pdivrMr //. apply: lt_trans (archi_boundP _) _; last by rewrite ltr_nat; raise_big_enough. by rewrite mulr_ge0 // invr_ge0 ltW. 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