proposition: Lemma Psucc_lt : forall p, (Zpos p < Zpos (Pos.succ p))%Z.
proof: Proof. intros. replace (Zpos (Pos.succ p)) with (1 + Zpos p)%Z. lia. induction p; trivial. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith