proposition: Lemma Sup_opp_inf (u : nat -> Rbar) : Sup_seq u = Rbar_opp (Inf_seq (fun n => Rbar_opp (u n))).
proof: Proof. rewrite /Inf_seq ; case: (ex_inf_seq _) => iu Hiu /=. apply is_sup_seq_unique. apply is_inf_opp_sup_seq. by rewrite Rbar_opp_involutive. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy