proposition: Lemma Sup_seq_ext (u v : nat -> Rbar) : (forall n, (u n) = (v n)) -> Sup_seq u = Sup_seq v.
proof: Proof. intro Heq ; rewrite {2}/Sup_seq ; case (ex_sup_seq v) ; simpl ; intros l2 Hv. by apply (is_sup_seq_unique u), is_sup_seq_ext with v. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy