proposition: Lemma is_lim_LimSup_seq (u : nat -> R) (l : Rbar) : is_lim_seq u l -> is_LimSup_seq u l.
proof: Proof. move /is_lim_seq_spec. case: l => [l | | ] /= Hu. move => eps ; case: (Hu eps) => {Hu} N Hu ; split. move => N0. exists (N + N0)%nat ; split. by apply MyNat.le_add_l. by apply Rabs_lt_between', Hu, Nat.le_add_r. exists N => n Hn. by apply Rabs_lt_between', Hu. move => M N0. case: (Hu M) => {Hu} N Hu. exists (N + N0)%nat ; split. by apply MyNat.le_add_l. by apply Hu, Nat.le_add_r. by []. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy