proposition: Lemma pow1_P_plus : forall a b, pow1_P (a + b) = pow1_P a * pow1_P b.
proof: Proof. intros a b. destruct a; destruct b; simpl; ring. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith