proposition: Lemma is_inf_seq_le (u v : nat -> Rbar) {l1 l2 : Rbar} : (forall n, Rbar_le (u n) (v n)) -> (is_inf_seq u l1) -> (is_inf_seq v l2) -> Rbar_le l1 l2.
proof: Proof. case: l1 => [l1 | | ] ; case: l2 => [l2 | | ] Hle Hu Hv ; case: (is_inf_seq_glb _ _ Hu) => {} Hu _ ; case: (is_inf_seq_glb _ _ Hv) => {Hv} _ Hv ; apply Hv => _ [n ->] ; apply Rbar_le_trans with (2 := Hle _), Hu ; by exists n. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy