proposition: Lemma Inf_seq_le (u v : nat -> Rbar) : (forall n, Rbar_le (u n) (v n)) -> Rbar_le (Inf_seq u) (Inf_seq v).
proof: Proof. move => Heq ; rewrite /Inf_seq ; case: (ex_inf_seq u) => l1 Hu ; case: (ex_inf_seq v) => /= l2 Hv. by apply (is_inf_seq_le u v). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy