proposition: Lemma nat_ind2 : forall (P : nat -> Prop), P O -> P (S O) -> (forall m, P m -> P (S (S m))) -> forall n, P n.
proof: Proof. intros P H0 H1 H n. assert (P n /\ P (S n)). induction n; split; try assumption; [ | apply H]; apply IHn. apply H2. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith