proposition: Lemma Inf_opp_sup (u : nat -> Rbar) : Inf_seq u = Rbar_opp (Sup_seq (fun n => Rbar_opp (u n))).
proof: Proof. rewrite Sup_opp_inf Rbar_opp_involutive. rewrite /Inf_seq. repeat (case: ex_inf_seq ; intros) => /=. apply is_inf_seq_glb in p. apply is_inf_seq_glb in p0. move: p p0 ; apply Rbar_is_glb_eq. move => x1 ; split ; case => n -> ; exists n ; by rewrite Rbar_opp_involutive. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy