proposition: Lemma pow1_nat : forall n, pow1 (Z_of_nat n) = (- 1) ^ n.
proof: Proof. intros n. destruct n. trivial. unfold Z_of_nat. simpl pow1. generalize dependent n; apply nat_ind2; try (simpl; trivial; ring). intros n H; simpl. rewrite pow1_P_ind. rewrite H. simpl pow; field. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith