proposition: Lemma Rseq_pow_abs_compat : forall r, Rseq_pow (Rabs r) == Rseq_abs (Rseq_pow r).
proof: Proof. intros r n ; unfold Rseq_pow, Rseq_abs ; apply RPow_abs. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_rewrite_facts MyRIneq MyReals Lra