proposition: Lemma Datan_seq_decreasing : forall x, -1 < x -> x < 1 -> Un_decreasing (Datan_seq x).
proof: Proof. intros x x_lb x_ub n. unfold Datan_seq. replace (2 * S n)%nat with (2 + 2 * n)%nat by ring. rewrite <- (Rmult_1_l (x ^ (2 * n))). rewrite pow_add. apply Rmult_le_compat_r. { rewrite pow_mult; apply pow_le, pow2_ge_0. } apply Rlt_le; rewrite <- pow2_abs. assert (intabs : 0 <= Rabs x < 1). { split;[apply Rabs_pos | apply Rabs_def1]; tauto. } apply (pow_lt_1_compat (Rabs x) 2) in intabs. { tauto. } lia. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia