proposition: Lemma Datan_seq_increasing : forall x y n, (n > 0)%nat -> 0 <= x < y -> Datan_seq x n < Datan_seq y n.
proof: Proof. intros x y n n_lb x_encad ; assert (x_pos : x >= 0) by intuition. assert (y_pos : y > 0). { apply Rle_lt_trans with (r2:=x) ; intuition. } induction n. { lia. } clear -x_encad x_pos y_pos ; induction n ; unfold Datan_seq. { case x_pos ; clear x_pos ; intro x_pos. { simpl ; apply Rmult_gt_0_lt_compat ; intuition. lra. } rewrite x_pos ; rewrite pow_i. { replace (y ^ (2*1)) with (y*y). { apply Rmult_gt_0_compat ; assumption. } simpl ; field. } intuition. } assert (Hrew : forall a, a^(2 * S (S n)) = (a ^ 2) * (a ^ (2 * S n))). { clear ; intro a ; replace (2 * S (S n))%nat with (S (S (2 * S n)))%nat by lia. simpl ; field. } case x_pos ; clear x_pos ; intro x_pos. { rewrite Hrew ; rewrite Hrew. apply Rmult_gt_0_lt_compat ; intuition. apply Rmult_gt_0_lt_compat ; intuition ; lra. } rewrite x_pos. rewrite pow_i. { intuition. } lia. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia