proposition: Lemma Rseq_abs_alt : forall An, Rseq_abs (Rseq_alt An) == Rseq_abs An.
proof: Proof. intros An n ; unfold Rseq_alt, Rseq_pow ; rewrite Rseq_abs_mult ; unfold Rseq_mult, Rseq_abs ; rewrite Rabs_opp1 ; apply Rmult_1_l. Qed.
imports: MyRIneq Rsequence_def