proposition: Lemma creal_z3seq : creal_axiom z3seq.
proof: Proof. rewrite /creal_axiom. pose n_inv_seq (n : nat) := n%:Q^-1. have [/= modulus_n_inv modulus_n_inv_P] : {asympt e : i / n_inv_seq i < e}. exists_big_modulus M rat => /=. move=> eps i lt_eps0 hMi. rewrite /n_inv_seq -div1r ltr_pdivrMr; last by rewrite ltr0n; raise_big_enough. rewrite -ltr_pdivrMl // mulr1. apply: lt_trans (archi_boundP _) _; first by rewrite ger0E ltW. rewrite ltr_nat; raise_big_enough. by close. exists_big_modulus m rat. move=> eps i j lt_eps_0 hmi hmj. wlog ltij : i j hmi hmj / (j < i)%N. move=> hwlog; case: (ltngtP i j); last by move ->; rewrite subrr. - rewrite distrC; exact/hwlog. - exact/hwlog. rewrite gtr0_norm; last exact: lt_0_Dz3seq. pose v (n : nat) := n%:Q ^- 2. have vpos (n : nat) : (0 < n)%N -> 0 < v n. by move=> ?; rewrite /v invr_gt0; apply: exprn_gt0; rewrite ltr0n. have maj : z3seq i - z3seq j <= - 2%:Q^-1 * \sum_(j <= k < i) (v (k + 1)%N - v k). rewrite Dz3seqE // big_add1 /= mulr_sumr. apply: ler_sum_nat => k /andP[hjk hki]; rewrite /v addn1. apply: z3seq_smd_maj; rewrite ltr0n; apply: leq_trans _ hjk. raise_big_enough. apply: le_lt_trans maj _; rewrite telescope_nat //. suff maj : v j < 2%:Q * eps. rewrite mulNr -mulrN opprB ltr_pdivrMl // ltrBlDr. apply: lt_trans maj _; rewrite ltrDl; apply: vpos; exact: ltn_trans ltij. have maj : v j < j%:Q^-1. rewrite /v -div1r ltr_pdivrMr; last by rewrite exprn_gt0 // ltr0n. by rewrite mulKf ?ltr1n // lt0r_neq0 // ltr0n. by apply: lt_trans maj _; apply: modulus_n_inv_P; rewrite // pmulr_rgt0. 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