proposition: Lemma Inf_le_sup (u : nat -> Rbar) : Rbar_le (Inf_seq u) (Sup_seq u).
proof: Proof. rewrite /Inf_seq ; case: (ex_inf_seq _) ; case => [iu | | ] Hiu ; rewrite /Sup_seq ; case: (ex_sup_seq _) ; case => [su | | ] Hsu //=. apply le_epsilon => e He ; set eps := mkposreal e He ; case: (Hiu (pos_div_2 eps)) => {} Hiu _ ; case: (Hsu (pos_div_2 eps)) => {} Hsu _ ; apply Rlt_le. have : (iu = iu - e/2 + e/2) ; first by ring. move => -> ; have : (su+e = su + e/2 + e/2) ; first by field. by move => -> ; apply Rplus_lt_compat_r, (Rbar_lt_trans (Finite (iu - e/2)) (u O) (Finite (su + e/2))). set eps := mkposreal _ Rlt_0_1 ; case: (Hiu eps) => {} Hiu _ ; move: (Hiu O) => {Hiu} ; apply Rbar_le_not_lt, Rbar_lt_le, Hsu. set eps := mkposreal _ Rlt_0_1 ; case: (Hsu eps) => {} Hsu _ ; move: (Hsu O) => {Hsu} ; apply Rbar_le_not_lt, Rbar_lt_le, Hiu. move: (Hiu 0 O) => {Hiu} ; apply Rbar_le_not_lt, Rbar_lt_le, Hsu. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy