proposition: Lemma Datan_seq_pos : forall x n, 0 < x -> 0 < Datan_seq x n.
proof: Proof. intros x n x_lb ; unfold Datan_seq ; induction n. { simpl ; intuition. } replace (x ^ (2 * S n)) with ((x ^ 2) * (x ^ (2 * n))). { apply Rmult_gt_0_compat. { replace (x^2) with (x*x) by field ; apply Rmult_gt_0_compat ; assumption. } assumption. } replace (2 * S n)%nat with (S (S (2 * n))) by lia. simpl ; field. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia