proposition: Lemma adjacent (u_ v_ : R ^nat) : nondecreasing_seq u_ -> nonincreasing_seq v_ -> v_ - u_ @ \oo --> (0 : R) -> [/\ limn v_ = limn u_, cvgn u_ & cvgn v_].
proof: Proof. set w_ := v_ - u_ => iu dv w0; have vu n : v_ n >= u_ n. suff : limn w_ <= w_ n by rewrite (cvg_lim _ w0)// subr_ge0. apply: (nonincreasing_cvgn_ge _ (cvgP _ w0)) => m p mp. by rewrite lerB; rewrite ?iu ?dv. have cu : cvgn u_. apply: nondecreasing_is_cvgn => //; exists (v_ 0%N) => _ [n _ <-]. by rewrite (le_trans (vu _)) // dv. have cv : cvgn v_. apply: nonincreasing_is_cvgn => //; exists (u_ 0%N) => _ [n _ <-]. by rewrite (le_trans _ (vu _)) // iu. by split=> //; apply/eqP; rewrite -subr_eq0 -limB //; exact/eqP/cvg_lim. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau