proposition: Lemma ex_inf_seq (u : nat -> Rbar) : {l : Rbar | is_inf_seq u l}.
proof: Proof. case : (ex_sup_seq (fun n => Rbar_opp (u n))) => l Hl. exists (Rbar_opp l) ; apply is_sup_opp_inf_seq ; by rewrite Rbar_opp_involutive. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy