proposition: Lemma is_sup_seq_le (u v : nat -> Rbar) {l1 l2 : Rbar} : (forall n, Rbar_le (u n) (v n)) -> (is_sup_seq u l1) -> (is_sup_seq v l2) -> Rbar_le l1 l2.
proof: Proof. destruct l1 as [l1 | | ] ; destruct l2 as [l2 | | ] ; intros Hle Hu Hv ; case (is_sup_seq_lub _ _ Hu) ; clear Hu ; intros _ Hu ; case (is_sup_seq_lub _ _ Hv) ; clear Hv ; intros Hv _ ; apply Hu ; intros x (n,Hn) ; rewrite Hn ; clear x Hn ; apply Rbar_le_trans with (1 := Hle _), Hv ; exists n ; auto. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy