proposition: Lemma Sup_seq_minor_le (u : nat -> Rbar) (M : R) (n : nat) : Rbar_le M (u n) -> Rbar_le M (Sup_seq u).
proof: Proof. intros H'. destruct (Rbar_le_lt_or_eq_dec _ _ H') as [H|H]. apply Rbar_lt_le. apply Sup_seq_minor_lt. by exists n. rewrite H. rewrite /Sup_seq ; case: ex_sup_seq => l Hl ; simpl proj1_sig. by apply is_sup_seq_major. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy