proposition: Lemma pow1_Rabs : forall z, Rabs (pow1 z) = 1.
proof: Proof. destruct z; try destruct p; simpl; change (-1) with (-(1%R)); try rewrite Rabs_Ropp; apply Rabs_R1. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith