proposition: Lemma Lim_seq_incr_1 (u : nat -> R) : Lim_seq (fun n => u (S n)) = Lim_seq u.
proof: Proof. rewrite /Lim_seq. replace (LimSup_seq (fun n : nat => u (S n))) with (LimSup_seq u). replace (LimInf_seq (fun n : nat => u (S n))) with (LimInf_seq u). by []. rewrite /LimInf_seq ; case: ex_LimInf_seq => l1 H1 ; case: ex_LimInf_seq => l2 H2 /= ; case: l1 H1 => [l1 | | ] /= H1 ; case: l2 H2 => [l2 | | ] /= H2. apply Rbar_finite_eq, Rle_antisym ; apply le_epsilon => e He ; set eps := mkposreal e He ; apply Rlt_le. case: (proj2 (H1 (pos_div_2 eps))) => /= {H1} N H1. case: (proj1 (H2 (pos_div_2 eps)) N) => /= {H2} n [Hn H2]. apply Rlt_trans with (u (S n) + e/2). replace l1 with ((l1-e/2)+e/2) by ring. apply Rplus_lt_compat_r. apply H1. apply Nat.le_trans with (1 := Hn). apply Nat.le_succ_diag_r. replace (l2+e) with ((l2+e/2)+e/2) by field. by apply Rplus_lt_compat_r, H2. case: (proj2 (H2 (pos_div_2 eps))) => /= {H2} N H2. case: (proj1 (H1 (pos_div_2 eps)) (S N)) => /= {H1} . case => [ | n] [Hn H1]. by apply Nat.nle_succ_0 in Hn. apply Rlt_trans with (u (S n) + e/2). replace l2 with ((l2-e/2)+e/2) by ring. apply Rplus_lt_compat_r. apply H2. by apply le_S_n, Hn. replace (l1+e) with ((l1+e/2)+e/2) by field. by apply Rplus_lt_compat_r, H1. have : False => //. case: (H2 (l1+1)) => {H2} N /= H2. case: (proj1 (H1 (mkposreal _ Rlt_0_1)) (S N)) ; case => /= {H1} [ | n] [Hn]. by apply Nat.nle_succ_0 in Hn. apply Rle_not_lt, Rlt_le, H2. by apply le_S_n. have : False => //. case: (proj2 (H1 (mkposreal _ Rlt_0_1))) => {H1} N /= H1. case: ((H2 (l1-1)) N) => /= {H2} n [Hn]. apply Rle_not_lt, Rlt_le, H1. by apply Nat.le_trans with (2 := Nat.le_succ_diag_r _). have : False => //. case: (H1 (l2+1)) => {H1} N /= H1. case: (proj1 (H2 (mkposreal _ Rlt_0_1)) N) => /= {H2} n [Hn]. apply Rle_not_lt, Rlt_le, H1. by apply Nat.le_trans with (2 := Nat.le_succ_diag_r _). by []. have : False => //. case: (H1 0) => {H1} N H1. case: (H2 0 N)=> {H2} n [Hn]. apply Rle_not_lt, Rlt_le, H1. by apply Nat.le_trans with (2 := Nat.le_succ_diag_r _). have : False => //. case: (proj2 (H2 (mkposreal _ Rlt_0_1))) => /= {H2} N H2. case: (H1 (l2-1) (S N)) ; case => [ | n] [Hn]. by apply Nat.nle_succ_0 in Hn. by apply Rle_not_lt, Rlt_le, H2, le_S_n. have : False => //. case: (H2 0) => {H2} N H2. case: (H1 0 (S N)) ; case => [ | n] [Hn]. by apply Nat.nle_succ_0 in Hn. by apply Rle_not_lt, Rlt_le, H2, le_S_n. by []. rewrite /LimSup_seq ; case: ex_LimSup_seq => l1 H1 ; case: ex_LimSup_seq => l2 H2 /= ; case: l1 H1 => [l1 | | ] /= H1 ; case: l2 H2 => [l2 | | ] /= H2. apply Rbar_finite_eq, Rle_antisym ; apply le_epsilon => e He ; set eps := mkposreal e He ; apply Rlt_le. case: (proj2 (H2 (pos_div_2 eps))) => /= {H2} N H2. case: ((proj1 (H1 (pos_div_2 eps))) (S N)) ; case => /= {H1} [ | n] [Hn H1]. by apply Nat.nle_succ_0 in Hn. replace l1 with ((l1-e/2)+e/2) by ring. replace (l2+e) with ((l2+e/2)+e/2) by field. apply Rplus_lt_compat_r. apply Rlt_trans with (1 := H1). by apply H2, le_S_n. case: (proj2 (H1 (pos_div_2 eps))) => /= {H1} N H1. case: ((proj1 (H2 (pos_div_2 eps))) N) => /= {H2} n [Hn H2]. replace l2 with ((l2-e/2)+e/2) by ring. replace (l1+e) with ((l1+e/2)+e/2) by field. apply Rplus_lt_compat_r. apply Rlt_trans with (1 := H2). by apply H1, Nat.le_trans with (2 := Nat.le_succ_diag_r _). have : False => //. case: (proj2 (H1 (mkposreal _ Rlt_0_1))) => /= {H1} N H1. case: (H2 (l1+1) N) => n [Hn]. by apply Rle_not_lt, Rlt_le, H1, Nat.le_trans with (2 := Nat.le_succ_diag_r _). have : False => //. case: (H2 (l1-1)) => {H2} N H2. case: (proj1 (H1 (mkposreal _ Rlt_0_1)) (S N)) ; case => [ | n] [Hn] /= . by apply Nat.nle_succ_0 in Hn. by apply Rle_not_lt, Rlt_le, H2, le_S_n. have : False => //. case: (proj2 (H2 (mkposreal _ Rlt_0_1))) => {H2} /= N H2. case: (H1 (l2+1) (S N)) ; case => [ | n] [Hn] /= . by apply Nat.nle_succ_0 in Hn. by apply Rle_not_lt, Rlt_le, H2, le_S_n. by []. have : False => //. case: (H2 0) => {H2} N H2. case: (H1 0 (S N)) ; case => [ | n] [Hn] /= . by apply Nat.nle_succ_0 in Hn. by apply Rle_not_lt, Rlt_le, H2, le_S_n. have : False => //. case: (H1 (l2-1)) => {H1} N H1. case: (proj1 (H2 (mkposreal _ Rlt_0_1)) N) => /= {H2} n [Hn]. by apply Rle_not_lt, Rlt_le, H1, Nat.le_trans with (2 := Nat.le_succ_diag_r _). have : False => //. case: (H1 0) => {H1} N H1. case: (H2 0 N) => {H2} n [Hn]. by apply Rle_not_lt, Rlt_le, H1, Nat.le_trans with (2 := Nat.le_succ_diag_r _). by []. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy