proposition: Lemma Sup_seq_le (u v : nat -> Rbar) : (forall n, Rbar_le (u n) (v n)) -> Rbar_le (Sup_seq u) (Sup_seq v).
proof: Proof. intros Heq ; unfold Sup_seq ; case (ex_sup_seq u) ; intros l1 Hu ; case (ex_sup_seq v) ; simpl ; intros l2 Hv. apply (is_sup_seq_le u v) ; auto. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy