proposition: Lemma is_LimInf_opp_LimSup_seq (u : nat -> R) (l : Rbar) : is_LimInf_seq (fun n => - u n) (Rbar_opp l) <-> is_LimSup_seq u l.
proof: Proof. case: l => [l | | ] /= ; split => Hl. move => eps ; case: (Hl eps) => {Hl} H1 H2 ; split. move => N ; case: (H1 N) => {H1} n [Hn H1]. exists n ; split. by []. apply Ropp_lt_cancel. apply Rlt_le_trans with (1 := H1) ; right ; ring. case: H2 => N H2. exists N => n Hn. apply Ropp_lt_cancel. apply Rle_lt_trans with (2 := H2 _ Hn) ; right ; ring. move => eps ; case: (Hl eps) => {Hl} H1 H2 ; split. move => N ; case: (H1 N) => {H1} n [Hn H1]. exists n ; split. by []. apply Ropp_lt_cancel ; rewrite Ropp_involutive. apply Rle_lt_trans with (2 := H1) ; right ; ring. case: H2 => N H2. exists N => n Hn. apply Ropp_lt_cancel ; rewrite Ropp_involutive. apply Rlt_le_trans with (1 := H2 _ Hn) ; right ; ring. move => M N. case: (Hl (-M) N) => {Hl} n [Hn Hl]. exists n ; split. by []. by apply Ropp_lt_cancel. move => M N. case: (Hl (-M) N) => {Hl} n [Hn Hl]. exists n ; split. by []. apply Ropp_lt_cancel ; by rewrite Ropp_involutive. move => M. case: (Hl (-M)) => {Hl} N Hl. exists N => n Hn. apply Ropp_lt_cancel. by apply Hl. move => M. case: (Hl (-M)) => {Hl} N Hl. exists N => n Hn. apply Ropp_lt_cancel ; rewrite Ropp_involutive. by apply Hl. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy