proposition: Lemma is_LimSup_seq_ind_1 (u : nat -> R) (l : Rbar) : is_LimSup_seq u l <-> is_LimSup_seq (fun n => u (S n)) l.
proof: Proof. case: l => [l | | ] ; split => //= Hu. move => eps. case: (Hu eps) => {Hu} H1 H2 ; split. move => N. case: (H1 (S N)) => {H1} n [Hn H1]. exists (pred n). case: (n) Hn H1 => /= [ | m] Hm H1. by apply Nat.nle_succ_0 in Hm. split. by apply le_S_n. by apply H1. case: H2 => N H2. exists N => n Hn. apply H2 ; intuition. move => eps. case: (Hu eps) => {Hu} H1 H2 ; split. move => N. case: (H1 N) => {H1} n [Hn H1]. exists (S n) ; intuition. case: H2 => N H2. exists (S N) => n Hn. case: (n) Hn => /= [ | m] Hm. by apply Nat.nle_succ_0 in Hm. apply H2 ; intuition. move => M N. case: (Hu M (S N)) => {Hu} n [Hn Hu]. exists (pred n). case: (n) Hn Hu => /= [ | m] Hm Hu. by apply Nat.nle_succ_0 in Hm. split. by apply le_S_n. by apply Hu. move => M N. case: (Hu M N) => {Hu} n [Hn Hu]. exists (S n) ; intuition. move => M. case: (Hu M) => {Hu} N Hu. exists N => n Hn. apply Hu ; intuition. move => M. case: (Hu M) => {Hu} N Hu. exists (S N) => n Hn. case: (n) Hn => /= [ | m] Hm. by apply Nat.nle_succ_0 in Hm. apply Hu ; intuition. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy