proposition: Lemma pow1_plus_nat : forall a b, pow1 (a + Z_of_nat b) = (pow1 a) * (-1) ^ b.
proof: Proof. intros. induction b. simpl; ring_simplify; inject; lia. rewrite inj_S; rewrite <- Zplus_succ_r_reverse; rewrite pow1_succ. rewrite IHb. simpl; ring. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith