proposition: Lemma pow1_succ : forall z, pow1 (Z.succ z) = - pow1 z.
proof: Proof. destruct z; trivial; destruct p; simpl; try ring; destruct p; simpl; ring. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith