proposition: Lemma is_sup_opp_inf_seq (u : nat -> Rbar) (l : Rbar) : is_sup_seq (fun n => Rbar_opp (u n)) (Rbar_opp l) <-> is_inf_seq u l.
proof: Proof. case: l => [l | | ] ; split => Hl. move => eps ; case: (Hl eps) => {Hl} [lb [n lub]] ; split. move => n0 ; apply Rbar_opp_lt ; have : (-(l-eps) = -l+eps) ; first by ring. by move => /= ->. exists n ; apply Rbar_opp_lt ; rewrite /= (Ropp_plus_distr l eps) ; apply lub. move => eps ; case: (Hl eps) => {Hl} [ub [n lub]] ; split. move => n0 ; have : (-(l-eps) = (-l+eps)) ; first by ring. move => /= <- ; by apply (Rbar_opp_lt (u n0) (Finite (l-eps))). exists n ; rewrite /Rminus -(Ropp_plus_distr l eps) ; by apply (Rbar_opp_lt (Finite (l+eps)) (u n)). move => M n ; apply Rbar_opp_lt, Hl. move => M n ; apply Rbar_opp_lt ; rewrite Rbar_opp_involutive ; apply Hl. move => M ; case: (Hl (-M)) => {Hl} n Hl ; exists n ; by apply Rbar_opp_lt. move => M ; case: (Hl (-M)) => {Hl} n Hl ; exists n ; apply Rbar_opp_lt ; by rewrite Rbar_opp_involutive. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy