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