proposition: Lemma ex_lim_seq_adj (u v : nat -> R) : (forall n, u n <= u (S n)) -> (forall n, v (S n) <= v n) -> is_lim_seq (fun n => v n - u n) 0 -> ex_finite_lim_seq u /\ ex_finite_lim_seq v /\ Lim_seq u = Lim_seq v.
proof: Proof. move => Hu Hv H0. suff H : forall n, u n <= v n. suff Eu : ex_finite_lim_seq u. split ; try auto. suff Ev : ex_finite_lim_seq v. split ; try auto. apply is_lim_seq_unique in H0. rewrite Lim_seq_minus in H0 ; try by intuition. apply ex_finite_lim_seq_correct in Eu. apply ex_finite_lim_seq_correct in Ev. rewrite -(proj2 Eu) -(proj2 Ev) /= in H0 |- *. apply Rbar_finite_eq in H0 ; apply Rbar_finite_eq. by apply sym_eq, Rminus_diag_uniq, H0. by apply ex_finite_lim_seq_correct. by apply ex_finite_lim_seq_correct. apply ex_finite_lim_seq_correct in Eu. apply ex_finite_lim_seq_correct in Ev. by rewrite -(proj2 Eu) -(proj2 Ev). apply ex_finite_lim_seq_decr with (u O) => //. move => n ; apply Rle_trans with (2 := H _). elim: n => [ | n IH]. by apply Rle_refl. by apply Rle_trans with (2 := Hu _). apply ex_finite_lim_seq_incr with (v O) => //. move => n ; apply Rle_trans with (1 := H _). elim: n => [ | n IH]. by apply Rle_refl. by apply Rle_trans with (1 := Hv _). move => n0 ; apply Rnot_lt_le ; move/Rminus_lt_0 => H. apply is_lim_seq_spec in H0. case: (H0 (mkposreal _ H)) => /= {H0} N H0. move: (H0 _ (MyNat.le_add_l N n0)) ; apply Rle_not_lt. rewrite Rminus_0_r ; apply Rle_trans with (2 := Rabs_maj2 _). rewrite Ropp_minus_distr'. apply Rplus_le_compat, Ropp_le_contravar. elim: (N) => [ | m IH]. rewrite Nat.add_0_r ; apply Rle_refl. rewrite -plus_n_Sm ; by apply Rle_trans with (2 := Hu _). elim: (N) => [ | m IH]. rewrite Nat.add_0_r ; apply Rle_refl. rewrite -plus_n_Sm ; by apply Rle_trans with (1 := Hv _). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy