proposition: Lemma is_inf_opp_sup_seq (u : nat -> Rbar) (l : Rbar) : is_inf_seq (fun n => Rbar_opp (u n)) (Rbar_opp l) <-> is_sup_seq u l.
proof: Proof. destruct l as [l | | ] ; split ; intros Hl. intro eps ; case (Hl eps) ; clear Hl ; intros lb (n, glb) ; split. intro n0 ; apply Rbar_opp_lt ; simpl ; rewrite (Ropp_plus_distr l eps) ; apply lb. exists n ; apply Rbar_opp_lt ; assert (Rw : -(l-eps) = -l+eps). ring. simpl ; rewrite Rw ; clear Rw ; auto. intro eps ; case (Hl eps) ; clear Hl ; intros ub (n, lub) ; split. intros n0 ; unfold Rminus ; rewrite <-(Ropp_plus_distr l eps) ; apply (Rbar_opp_lt (Finite (l+eps)) (u n0)) ; simpl ; apply ub. exists n ; assert (Rw : -(l-eps) = -l+eps). ring. simpl ; rewrite <-Rw ; apply (Rbar_opp_lt (u n) (Finite (l-eps))) ; auto. intro M ; case (Hl (-M)) ; clear Hl ; intros n Hl ; exists n ; apply Rbar_opp_lt ; auto. intro M ; case (Hl (-M)) ; clear Hl ; intros n Hl ; exists n ; apply Rbar_opp_lt ; rewrite Rbar_opp_involutive ; auto. intros M n ; apply Rbar_opp_lt, Hl. intros M n ; apply Rbar_opp_lt ; rewrite Rbar_opp_involutive ; apply Hl. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy