Require Import Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts.
Require Import Rpser_def Rpser_def_simpl.
Require Import MyRIneq MyNat Fourier.

Open Scope R_scope.
Open Scope Rseq_scope.

Lemma Rseq_sum_ext_strong : ∀ Un Vn n,
  (∀ p, (p ≤ n)%nat → Un p = Vn p) →
  Rseq_sum Un n = Rseq_sum Vn n.
Proof.
intros Un Vn n ; induction n ; intro Heq.
 simpl ; apply Heq ; trivial.
 do 2 rewrite Rseq_sum_simpl ; rewrite IHn, Heq.
  reflexivity.
  trivial.
  intros ; apply Heq ; auto.
Qed.

Lemma Rseq_sum_ext : ∀ Un Vn,
  Un == Vn → Rseq_sum Un == Rseq_sum Vn.
Proof.
intros Un Vn Heq n ; apply Rseq_sum_ext_strong ; trivial.
Qed.

Lemma Rseq_sum_scal_compat_l : ∀ (l : R) Un,
  Rseq_sum (l × Un) == l × (Rseq_sum Un).
Proof.
intros l Un n ; induction n.
 reflexivity.
 simpl ; rewrite IHn ;
  unfold Rseq_mult, Rseq_constant ;
  simpl ; ring.
Qed.

Lemma Rseq_sum_constant_compat: ∀ (l : R) n,
  (Rseq_sum l n = INR (S n) × l)%R.
Proof.
intros l n ; induction n.
 simpl ; symmetry ; apply Rmult_1_l.
 rewrite Rseq_sum_simpl, S_INR, IHn ; unfold Rseq_constant ; ring.
Qed.

Lemma Rseq_sum_scal_compat_r : ∀ (l : R) Un,
  Rseq_sum (Un × l) == Rseq_sum Un × l.
Proof.
intros l Un n ; induction n.
 reflexivity.
 simpl ; rewrite IHn ;
  unfold Rseq_mult, Rseq_constant ;
  simpl ; ring.
Qed.

Lemma Rseq_sum_opp_compat : ∀ Un,
  Rseq_sum (- Un) == - Rseq_sum Un.
Proof.
intros Un n ; induction n.
 reflexivity.
 simpl ; rewrite IHn ;
  unfold Rseq_opp ;
  simpl ; ring.
Qed.

Lemma Rseq_sum_plus_compat : ∀ Un Vn,
  Rseq_sum (Un + Vn) == Rseq_sum Un + Rseq_sum Vn.
Proof.
intros Un Vn n ; induction n.
 reflexivity.
 simpl ; rewrite IHn ;
  unfold Rseq_plus ; simpl ;
  ring.
Qed.

Lemma Rseq_sum_minus_compat : ∀ Un Vn,
  Rseq_sum (Un - Vn) == Rseq_sum Un - Rseq_sum Vn.
Proof.
intros Un Vn n ; rewrite Rseq_sum_ext with (Un - Vn) (Un + (- Vn)) _,
 Rseq_sum_plus_compat.
 unfold Rseq_plus, Rseq_minus ; rewrite Rseq_sum_opp_compat ; reflexivity.
 unfold Rseq_minus ; intro ; reflexivity.
Qed.

Lemma Rseq_sum_shift_compat : ∀ Un n,
  Rseq_sum (Rseq_shift Un) n = (Rseq_shift (Rseq_sum Un) n - Un O)%R.
Proof.
intros Un n ; induction n ;
 [| simpl ; rewrite IHn] ;
 unfold Rseq_shift, Rseq_minus ; simpl ; ring.
Qed.

Lemma Rseq_sum_shifts_compat : ∀ Un k n,
  Rseq_sum (Rseq_shifts Un (S k)) n = (Rseq_shifts (Rseq_sum Un) (S k) n - Rseq_sum Un k)%R.
Proof.
intros Un k n ; induction n.
 unfold Rseq_shifts, Rseq_minus ; simpl ; rewrite plus_0_r ; ring.
 simpl ; rewrite IHn ; unfold Rseq_minus, Rseq_shifts ;
  simpl ; rewrite <- (plus_n_Sm k n) ; simpl ; ring.
Qed.

Lemma Rseq_sum_split_compat : ∀ Un k n, (k < n)%nat →
  (Rseq_sum Un n = Rseq_sum Un k + Rseq_sum (Rseq_shifts Un (S k)) (n - S k))%R.
Proof.
intros Un k n kltn ; rewrite Rseq_sum_shifts_compat ; ring_simplify.
 unfold Rseq_shifts ; rewrite le_plus_minus_r ; [reflexivity | omega].
Qed.

Lemma Rseq_sum_reindex_compat : ∀ Un n,
  Rseq_sum Un n = Rseq_sum (fun i ⇒ Un (n - i)%nat) n.
Proof.
intros Un n ; revert Un ; induction n ; intro Un.
 reflexivity.
 do 2 rewrite Rseq_sum_simpl.
 rewrite (IHn (fun i ⇒ Un (S n - i)%nat)), minus_diag.
 rewrite (Rseq_sum_ext_strong (fun i ⇒ Un (S n - (n - i))%nat) (Rseq_shift Un)).
 rewrite Rseq_sum_shift_compat ; unfold Rseq_shift ; simpl ; ring.
 intros m m_bd ; unfold Rseq_shift ; replace (S n - (n - m))%nat with (S m) by omega ;
 reflexivity.
Qed.

Lemma Rseq_prod_comm: ∀ An Bn, (An # Bn == Bn # An)%Rseq.
Proof.
intros An Bn n ; unfold Rseq_prod, Rseq_mult ;
 rewrite Rseq_sum_reindex_compat ; apply Rseq_sum_ext_strong ;
 intros p p_ub ; replace (n - (n - p))%nat with p by omega ;
 ring.
Qed.

Lemma Rseq_sum_prod_compat: ∀ An Bn n,
  Rseq_sum (An # Bn) n =
  Rseq_sum (fun i ⇒ (Rseq_sum Bn i) × An (n - i)%nat)%R n.
Proof.
intros An Bn n ; induction n.
 unfold Rseq_prod, Rseq_mult ; simpl ; apply Rmult_comm.
 transitivity (Rseq_sum ((fun i ⇒ (An i × (Rseq_sum Bn (n - i)%nat))%R) +
  (fun i ⇒ (An i × Bn (S (n - i))%nat))%R)%Rseq n + An (S n) × Bn O)%R.
 rewrite Rseq_sum_plus_compat, Rseq_sum_simpl, IHn ; unfold Rseq_plus ;
 rewrite Rplus_assoc ; apply Rplus_eq_compat.
 rewrite Rseq_sum_reindex_compat ; apply Rseq_sum_ext_strong ;
  intros p p_ub ; replace (n - (n - p))%nat with p by omega ; apply Rmult_comm.
 replace O with ((S n) - S n)%nat by omega ; unfold Rseq_prod ;
  rewrite Rseq_sum_simpl ; apply Rplus_eq_compat_r ; apply Rseq_sum_ext_strong ;
  intros p p_ub ; unfold Rseq_mult ; replace (S n - p)%nat with (S (n - p)) by omega ;
  reflexivity.
 transitivity (Rseq_sum (fun i ⇒ (An i × (Rseq_sum Bn (S n - i)))%R) (S n)).
 rewrite Rseq_sum_simpl, minus_diag ; apply Rplus_eq_compat ; [| trivial].
 apply Rseq_sum_ext_strong ; intros p p_ub ; unfold Rseq_plus ;
 replace (S n - p)%nat with (S (n - p)) by omega ; rewrite Rseq_sum_simpl ; ring.
 rewrite Rseq_sum_reindex_compat ; apply Rseq_sum_ext_strong ; intros p p_ub ;
 replace (S n - (S n - p))%nat with p by omega ; apply Rmult_comm.
Qed.

Lemma two_Sn : ∀ n, (2 × S n = S (S (2 × n)))%nat.
Proof.
intro n ; ring.
Qed.

Lemma Rseq_sum_zip_compat_odd : ∀ An Bn n,
  (Rseq_sum (Rseq_zip An Bn) (S (2 × n)) = Rseq_sum An n + Rseq_sum Bn n)%R.
Proof.
intros An Bn ; induction n.
 unfold Rseq_zip ; simpl.
  case (n_modulo_2 0) ; intros [p Hp] ; [| apply False_ind ; omega].
  case (n_modulo_2 1) ; intros [q Hq] ; [apply False_ind ; omega |].
  assert (Hp' : p = O) by omega ; assert (Hq' : q = O) by omega ; subst ; reflexivity.
 rewrite two_Sn ; do 2 rewrite Rseq_sum_simpl ; rewrite IHn ; do 2 rewrite Rseq_sum_simpl.
  repeat rewrite Rplus_assoc ; apply Rplus_eq_compat_l.
  rewrite (Rplus_comm (An (S n))), Rplus_assoc ; apply Rplus_eq_compat_l.
  rewrite Rplus_comm, <- two_Sn ; apply Rplus_eq_compat ; unfold Rseq_zip ;
   [ case (n_modulo_2 (S (2 × S n))) ; intros [p Hp] ; [apply False_ind ; omega |] |
     case (n_modulo_2 (2 × S n)) ; intros [p Hp] ; [| apply False_ind ; omega] ] ;
   assert (Hp' : p = S n) by omega ; subst ; reflexivity.
Qed.

Lemma Rseq_sum_zip_compat_even : ∀ An Bn n,
  (Rseq_sum (Rseq_zip An Bn) (2 × S n) = Rseq_sum An (S n) + Rseq_sum Bn n)%R.
Proof.
intros An Bn n ; rewrite two_Sn, Rseq_sum_simpl, Rseq_sum_zip_compat_odd,
 Rseq_sum_simpl, <- two_Sn ; unfold Rseq_zip.
 case (n_modulo_2 (2 × S n)) ; intros [p Hp] ; [| apply False_ind ; omega].
 assert (Hp' : p = S n) by omega ; subst ; ring.
Qed.

Lemma Rseq_sum_pos_strong : ∀ An n,
  (∀ p, (p ≤ n)%nat → 0 ≤ An p) →
  0 ≤ Rseq_sum An n.
Proof.
intros An n ; induction n ; intro Hpos.
 simpl ; apply Hpos ; trivial.
 rewrite Rseq_sum_simpl ; apply Rplus_le_le_0_compat ;
 [apply IHn ; intros p p_bd |] ; apply Hpos ; omega.
Qed.

Lemma Rseq_sum_pos: ∀ An n,
 (∀ n, 0 ≤ An n) → 0 ≤ Rseq_sum An n.
Proof.
intros ; apply Rseq_sum_pos_strong ; trivial.
Qed.

Lemma Rseq_sum_le_compat_strong: ∀ An Bn n,
 (∀ p, (p ≤ n)%nat → An p ≤ Bn p) →
 Rseq_sum An n ≤ Rseq_sum Bn n.
Proof.
intros An Bn n Hle ; induction n.
 simpl ; apply Hle ; trivial.
 simpl ; transitivity (Rseq_sum Bn n + An (S n))%R.
  apply Rplus_le_compat_r ; apply IHn ; auto.
  apply Rplus_le_compat_l ; apply Hle ; trivial.
Qed.

Lemma Rseq_sum_le_compat: ∀ An Bn n,
 (∀ n, An n ≤ Bn n) → Rseq_sum An n ≤ Rseq_sum Bn n.
Proof.
intros ; apply Rseq_sum_le_compat_strong ; trivial.
Qed.

Lemma Rseq_sum_lt_compat_strong: ∀ An Bn n,
 (∀ p, (p ≤ n)%nat → An p < Bn p) →
 Rseq_sum An n < Rseq_sum Bn n.
Proof.
intros An Bn n Hlt ; induction n.
 simpl ; apply Hlt ; trivial.
 simpl ; transitivity (Rseq_sum Bn n + An (S n))%R.
  apply Rplus_lt_compat_r ; apply IHn ; auto.
  apply Rplus_lt_compat_l ; apply Hlt ; trivial.
Qed.

Lemma Rseq_sum_lt_compat: ∀ An Bn n,
 (∀ n, An n < Bn n) → Rseq_sum An n < Rseq_sum Bn n.
Proof.
intros ; apply Rseq_sum_lt_compat_strong ; trivial.
Qed.

Lemma Rseq_sum_triang: ∀ An n,
  Rabs (Rseq_sum An n) ≤ Rseq_sum (| An |) n.
Proof.
intros An n ; induction n.
 unfold Rseq_abs ; simpl ; reflexivity.
 do 2 rewrite Rseq_sum_simpl ; eapply Rle_trans ;
 [eapply Rabs_triang |] ; apply Rplus_le_compat ;
 [assumption | reflexivity].
Qed.

Lemma Rseq_sum_lower_bound : ∀ An n lb,
  (∀ m, (m ≤ n)%nat → lb ≤ An m) →
  INR (S n) × lb ≤ Rseq_sum An n.
Proof.
intros An n lb HAn ; induction n.
 simpl ; rewrite Rmult_1_l ; apply HAn ; reflexivity.
 rewrite S_INR, Rmult_plus_distr_r, Rmult_1_l, Rseq_sum_simpl ;
  apply Rplus_le_compat ; [apply IHn | apply HAn ; reflexivity].
  intros m m_lb ; apply HAn ; omega.
Qed.

Lemma Rseq_sum_upper_bound : ∀ An n ub,
  (∀ m, (m ≤ n)%nat → An m ≤ ub) →
  Rseq_sum An n ≤ INR (S n) × ub.
Proof.
intros An n ub HAn ; induction n.
 simpl ; rewrite Rmult_1_l ; apply HAn ; reflexivity.
 rewrite S_INR, Rmult_plus_distr_r, Rmult_1_l, Rseq_sum_simpl ;
  apply Rplus_le_compat ; [apply IHn | apply HAn ; reflexivity].
  intros m m_lb ; apply HAn ; omega.
Qed.

Lemma Rseq_cv_pos_infty_criteria : ∀ An d, 0 < d →
  (∀ n, 0 ≤ An n) →
  (∀ M, ∃ N, (N ≥ M)%nat ∧ d ≤ Rseq_sum (Rseq_shifts An M) (N - M)) →
  Rseq_cv_pos_infty (Rseq_sum An).
Proof.
intros An d d_pos An_pos HAn.
 assert (HAn' : ∀ M, ∃ N, ∀ n, (N < n)%nat → INR M × d ≤ Rseq_sum An n).
  intro M ; induction M.
   destruct (HAn O) as [N [_ HN]] ; ∃ N.
   intros n n_lb ; simpl ; rewrite Rmult_0_l.
    rewrite (Rseq_sum_split_compat _ _ _ n_lb) ; apply Rplus_le_le_0_compat.
     transitivity d.
      left ; assumption.
      rewrite (minus_n_O N) ; erewrite Rseq_sum_ext ;
       [| symmetry ; eapply Rseq_shifts_0 ] ; assumption.
     apply Rseq_sum_pos ; intros ; apply An_pos.
    destruct IHM as [N HN] ; destruct (HAn (S (S N))) as [N' [N'_lb HN']] ; ∃ N' ;
     assert (N'_lb' : (S N < N')%nat) by omega.
    intros n n_lb ; rewrite S_INR, Rmult_plus_distr_r, Rmult_1_l,
     (Rseq_sum_split_compat _ _ _ n_lb), (Rseq_sum_split_compat _ _ _ N'_lb'),
     Rplus_assoc.
    apply Rplus_le_compat.
     apply HN ; auto.
     rewrite <- (Rplus_0_r d) ; apply Rplus_le_compat.
      apply HN'.
      apply Rseq_sum_pos ; intros ; apply An_pos.
 intro B ; pose (M := up (Rabs B / d)) ; destruct (archimed (Rabs B / d)) as [HB _].
  assert (M_pos : (0 ≤ M)%Z).
   apply le_IZR ; simpl ; eapply Rle_trans ; [| left ; eassumption].
   apply Rle_mult_inv_pos ; [apply Rabs_pos | assumption].
  destruct (IZN _ M_pos) as [M' HM'] ; destruct (HAn' M') as [N HN] ; ∃ (S N) ; intros n n_lb.
   apply Rlt_le_trans with (INR M' × d)%R ; [| apply HN ; omega].
   apply Rle_lt_trans with (Rabs B) ; [apply Rle_abs |].
   rewrite <- (Rmult_1_r (Rabs B)), <- (Rinv_l d), <- Rmult_assoc, INR_IZR_INZ, <- HM'.
   apply Rmult_lt_compat_r ; [assumption | apply HB].
   apply Rgt_not_eq ; assumption.
Qed.

Lemma Rseq_cv_neg_infty_criteria : ∀ An d, d < 0 →
  (∀ n, An n ≤ 0) →
  (∀ M, ∃ N, (N ≥ M)%nat ∧ Rseq_sum (Rseq_shifts An M) (N - M) ≤ d) →
  Rseq_cv_neg_infty (Rseq_sum An).
Proof.
intros An d d_neg An_neg HAn ; apply Rseq_cv_neg_infty_eq_compat with (- Rseq_sum (- An)).
 intro n ; unfold Rseq_opp at 1 ; rewrite Rseq_sum_opp_compat ; unfold Rseq_opp ;
 apply Ropp_involutive.
 apply Rseq_cv_pos_infty_opp_compat, Rseq_cv_pos_infty_criteria with (- d)%R.
  fourier.
  intro n ; unfold Rseq_opp ; pose (An_neg n) ; fourier.
  intro M ; destruct (HAn M) as [N [N_lb HN]] ; ∃ N ; split.
   assumption.
   rewrite Rseq_sum_ext with (Vn := - Rseq_shifts An M).
    rewrite Rseq_sum_opp_compat ; apply Ropp_le_contravar, HN.
    apply Rseq_shifts_opp_compat.
Qed.

Lemma Rseq_sum_even_odd_split : ∀ (An : Rseq) n,
  (Rseq_sum (fun i ⇒ An (2 × i)%nat) n +
  Rseq_sum (fun i ⇒ An (S (2 × i))%nat) n
  = Rseq_sum An (S (2 × n)))%R.
Proof.
intros An n ; induction n.
 reflexivity.
 replace (2 × (S n))%nat with (S (S (2 × n))) by ring.
 do 4 rewrite Rseq_sum_simpl.
 replace (2 × (S n))%nat with (S (S (2 × n))) by ring.
 rewrite <- IHn ; ring.
Qed.

Lemma Rseq_sum_even_odd_split' : ∀ An n,
  (Rseq_sum (fun i ⇒ An (2 × i)%nat) (S n) +
  Rseq_sum (fun i ⇒ An (S (2 × i))) n
  = Rseq_sum An (2 × (S n)))%R.
Proof.
intros An n ; replace (2 × S n)%nat with (S (S (2 × n))) by ring ;
 do 2 rewrite Rseq_sum_simpl ; rewrite <- Rseq_sum_even_odd_split ;
 replace (2 × S n)%nat with (S (S (2 × n))) by ring ; ring.
Qed.

Section Rseq_pps_facts.

Lemma Rseq_pps_simpl : ∀ An x n,
  Rseq_pps An x (S n) = (Rseq_pps An x n + (An (S n) × pow x (S n)))%R.
Proof.
intros ; reflexivity.
Qed.

Lemma Rseq_pps_0_simpl : ∀ An n,
 Rseq_pps An 0 n = An O.
Proof.
intros An n ; induction n.
 unfold Rseq_pps, gt_pser, Rseq_mult ; simpl ;
  rewrite Rmult_1_r ; reflexivity.
 rewrite Rseq_pps_simpl, IHn, pow_i ; [ring | omega].
Qed.

Lemma Rseq_pps_O_simpl : ∀ An x,
  Rseq_pps An x O = An O.
Proof.
intros An x ; unfold Rseq_pps ; apply gt_pser_0.
Qed.

Lemma Rseq_pps_ext : ∀ An Bn x,
  (An == Bn)%Rseq →
  (Rseq_pps An x == Rseq_pps Bn x)%Rseq.
Proof.
intros An Bn x Hext ; apply Rseq_sum_ext ;
 intro n ; unfold gt_pser, Rseq_mult ; rewrite Hext ;
 reflexivity.
Qed.

Lemma Rseq_pps_scal_compat_l : ∀ (l : R) An x,
  (Rseq_pps (l × An) x == l × Rseq_pps An x)%Rseq.
Proof.
intros l An x n ; unfold Rseq_pps ;
 rewrite Rseq_sum_ext with _ (l × (An × (pow x)))%Rseq _.
 apply Rseq_sum_scal_compat_l.
 clear ; intro n ; unfold gt_pser, Rseq_mult, Rseq_constant ;
  ring.
Qed.

Lemma Rseq_pps_scal_compat_r : ∀ (l : R) An x,
  (Rseq_pps (An × l) x == Rseq_pps An x × l)%Rseq.
Proof.
intros l An x n ; unfold Rseq_pps ;
 rewrite Rseq_sum_ext with _ ((An × (pow x)) × l)%Rseq _.
 apply Rseq_sum_scal_compat_r.
 clear ; intro n ; unfold gt_pser, Rseq_mult, Rseq_constant ;
  ring.
Qed.

Lemma Rseq_pps_opp_compat : ∀ An x,
  (Rseq_pps (- An) x == - Rseq_pps An x)%Rseq.
Proof.
intros An x n ; unfold Rseq_pps ;
 rewrite Rseq_sum_ext with _ (- (An × (pow x))) _.
 apply Rseq_sum_opp_compat.
 clear ; intro n ; unfold gt_pser, Rseq_mult, Rseq_opp ;
  ring.
Qed.

Lemma Rseq_pps_plus_compat : ∀ An Bn x,
  Rseq_pps (An + Bn) x == Rseq_pps An x + Rseq_pps Bn x.
Proof.
intros An Bn x n ; unfold Rseq_pps ;
 rewrite Rseq_sum_ext with _ ((An × (pow x)) + (Bn × (pow x))) _.
 apply Rseq_sum_plus_compat.
 clear ; intro n ; unfold gt_pser, Rseq_mult, Rseq_plus ;
  ring.
Qed.

Lemma Rseq_pps_abs_unfold : ∀ An x,
  Rseq_pps_abs An x == Rseq_pps (| An |) (Rabs x).
Proof.
intros An x ; apply Rseq_sum_ext ; apply gt_abs_pser_unfold.
Qed.

Lemma Rseq_pps_prod_unfold: ∀ An Bn x,
  Rseq_pps (An # Bn) x == Rseq_sum (gt_pser An x # (gt_pser Bn x)).
Proof.
intros An Bn x n ; induction n.
 unfold Rseq_pps, gt_pser, Rseq_prod, Rseq_mult ; simpl ; ring.
 rewrite Rseq_sum_simpl, Rseq_pps_simpl, IHn ; apply Rplus_eq_compat_l.
 etransitivity.
 symmetry ; eapply (Rseq_sum_scal_compat_r _ _ (S n)).
 apply Rseq_sum_ext_strong ; fold (pow x (S n)) ; intros p p_lb ;
 unfold gt_pser, Rseq_mult, Rseq_constant.
 replace (S n) with (p + (S n - p))%nat by omega ; rewrite pow_add ;
 replace (p + (S n - p) -p)%nat with (S n - p)%nat by omega ; ring.
Qed.

Lemma Rseq_pps_zip_compat_odd : ∀ An Bn x n,
  (Rseq_pps (Rseq_zip An Bn) x (S (2 × n)) =
  Rseq_pps An (x ^ 2) n + x × Rseq_pps Bn (x ^ 2) n)%R.
Proof.
intros An Bn x n ; unfold Rseq_pps ; erewrite Rseq_sum_ext ; [| eapply gt_pser_zip_compat] ;
 rewrite Rseq_sum_zip_compat_odd, Rseq_sum_scal_compat_l ; reflexivity.
Qed.

Lemma Rseq_pps_zip_compat_even : ∀ An Bn x n,
  (Rseq_pps (Rseq_zip An Bn) x (2 × S n) =
  Rseq_pps An (x ^ 2) (S n) + x × Rseq_pps Bn (x ^ 2) n)%R.
Proof.
intros An Bn x n ; unfold Rseq_pps ; erewrite Rseq_sum_ext ; [| eapply gt_pser_zip_compat] ;
 rewrite Rseq_sum_zip_compat_even, Rseq_sum_scal_compat_l ; reflexivity.
Qed.

Lemma unfold_Ropp : ∀ x, (- x = - 1 × x)%R.
Proof.
intros ; ring.
Qed.

Lemma Rseq_pps_alt_compat : ∀ An x,
  Rseq_pps (Rseq_alt An) x == Rseq_pps An (- x).
Proof.
intros An x n ; induction n.
 do 2 rewrite Rseq_pps_O_simpl ; unfold Rseq_alt, Rseq_mult, Rseq_pow ;
  apply Rmult_1_l.
 do 2 rewrite Rseq_pps_simpl ; rewrite IHn ; apply Rplus_eq_compat_l.
  unfold Rseq_alt, Rseq_mult, Rseq_pow ;
  rewrite (unfold_Ropp x), Rpow_mult_distr ; ring.
Qed.

Lemma Rpser_abs_unfold : ∀ An r l,
  Rpser_abs An r l ↔ Rpser (| An |) (Rabs r) l.
Proof.
intros An r l ; split ; intro Hyp ; unfold Rpser, Rpser_abs ;
assert (tmp := Rseq_pps_abs_unfold An r) ; eapply Rseq_cv_eq_compat ;
eauto ; symmetry ; assumption.
Qed.

End Rseq_pps_facts.