proposition: Lemma Rseq_cv_neg_infty_plus_compat : Rseq_cv_neg_infty Un -> Rseq_cv_neg_infty Vn -> Rseq_cv_neg_infty (Un + Vn).
proof: Proof. intros Hu Hv M. destruct (Hu (M / 2)%R) as [Nu HNu]. destruct (Hv (M / 2)%R) as [Nv HNv]. exists (Nat.max Nu Nv); intros n Hn. unfold Rseq_plus. replace M with (M / 2 + M / 2)%R by field. apply Rplus_lt_compat. apply HNu; eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. apply HNv; eapply Nat.le_trans; [apply Nat.le_max_r|eexact Hn]. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra