proposition: Lemma is_sup_seq_unique (u : nat -> Rbar) (l : Rbar) : is_sup_seq u l -> Sup_seq u = l.
proof: Proof. move => Hl ; rewrite /Sup_seq ; case: (ex_sup_seq _) => l0 Hl0 /= ; case: l Hl => [l | | ] Hl ; case: l0 Hl0 => [l0 | | ] Hl0 //. apply Rbar_finite_eq, Rle_antisym ; apply le_epsilon => e He ; set eps := mkposreal e He ; apply Rlt_le ; case: (Hl (pos_div_2 eps)) => {} Hl [n Hn] ; case: (Hl0 (pos_div_2 eps)) => {} Hl0 [n0 Hn0]. have: (l0 = (l0 - eps/2) + eps/2) ; [by field | move => -> ] ; have : (l + e = (l + eps/2) + eps/2) ; [ simpl ; field | move => -> ] ; apply Rplus_lt_compat_r, (Rbar_lt_trans (Finite (l0 - eps/2)) (u n0) (Finite (l + eps/2)) Hn0 (Hl _)). have: (l = (l - eps/2) + eps/2) ; [by field | move => -> ] ; have : (l0 + e = (l0 + eps/2) + eps/2) ; [ simpl ; field | move => -> ] ; apply Rplus_lt_compat_r, (Rbar_lt_trans (Finite (l - eps/2)) (u n) (Finite (l0 + eps/2)) Hn (Hl0 _)). case: (Hl0 (l + 1)) => n {} Hl0 ; contradict Hl0 ; apply Rbar_le_not_lt, Rbar_lt_le, (Hl (mkposreal _ Rlt_0_1)). case: (Hl (mkposreal _ Rlt_0_1)) => {Hl} _ [n Hl] ; contradict Hl ; apply Rbar_le_not_lt, Rbar_lt_le, Hl0. case: (Hl (l0 + 1)) => n {} Hl ; contradict Hl ; apply Rbar_le_not_lt, Rbar_lt_le, (Hl0 (mkposreal _ Rlt_0_1)). case: (Hl 0) => n {} Hl ; contradict Hl ; apply Rbar_le_not_lt, Rbar_lt_le, Hl0. case: (Hl0 (mkposreal _ Rlt_0_1)) => {Hl0} _ [n Hl0] ; contradict Hl0 ; apply Rbar_le_not_lt, Rbar_lt_le, Hl. case: (Hl0 0) => n {} Hl0 ; contradict Hl0 ; apply Rbar_le_not_lt, Rbar_lt_le, Hl. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy