proposition: Lemma Rseq_sandwich_theorem : forall Un Vn Wn l, (Rseq_cv Un l) -> (Rseq_cv Wn l) -> (forall n, Un n <= Vn n <= Wn n) -> Rseq_cv Vn l.
proof: Proof. intros Un Vn Wn l Hu Hw H eps Heps. destruct (Hu eps Heps) as [Nu HNu]. destruct (Hw eps Heps) as [Nw HNw]. exists (Nat.max Nu Nw); intros n Hn. eapply Rle_lt_trans. apply RmaxAbs; apply Rplus_le_compat_r; apply (H n). unfold Rmax; destruct Rle_dec as [_|_]. apply HNw; eapply Nat.le_trans; [apply Nat.le_max_r|eassumption]. apply HNu; eapply Nat.le_trans; [apply Nat.le_max_l|eassumption]. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra