proposition: Lemma Datan_seq_CV_0 : forall x, -1 < x -> x < 1 -> Un_cv (Datan_seq x) 0.
proof: Proof. intros x x_lb x_ub eps eps_pos. assert (x_ub2 : Rabs (x^2) < 1). { rewrite Rabs_pos_eq;[ | apply pow2_ge_0]. rewrite <- pow2_abs. assert (H: 0 <= Rabs x < 1) by (split;[apply Rabs_pos | apply Rabs_def1; auto]). apply (pow_lt_1_compat _ 2) in H;[tauto | lia]. } elim (pow_lt_1_zero (x^2) x_ub2 eps eps_pos) ; intros N HN ; exists N ; intros n Hn. unfold Rdist, Datan_seq. replace (x ^ (2 * n) - 0) with ((x ^ 2) ^ n). { apply HN ; assumption. } rewrite pow_mult ; field. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia