proposition: Lemma lub_cara : forall E l, is_lub E l -> forall e : posreal, ~ ~ (exists x, E x /\ l - e < x).
proof: Proof. intros E l H e. intro H0. assert (forall x, ~ (E x /\ l - e < x)) as H1. intros x Hx. apply H0 ; now exists x. clear H0. unfold is_lub in H. destruct H as (H, H0). assert ( ~ is_upper_bound E (l-e)) as H2. intro H2. apply H0 in H2. assert (0 < e) as H3. apply (cond_pos e). assert (l > l - e) as H4. apply tech_Rgt_minus. assumption. unfold Rgt in H4. destruct H2 as [H2 | H2]. assert (l < l) as H5. now apply Rlt_trans with (l-e). apply Rlt_irrefl in H5 ; contradiction. rewrite <- H2 in H4. apply Rlt_irrefl in H4 ; contradiction. unfold is_upper_bound in H2. assert (forall x : R, E x -> x <= l-e) as H3. clear H0 ; clear H. intro x. assert (~ (E x /\ l - e < x)) as H. apply H1. clear H1. intro H0. assert ({l-e<x}+{l-e=x}+{l-e>x}). apply total_order_T. destruct H1 as [H1 | H1]. destruct H1 as [H1 | H1]. assert (E x /\ l-e < x). now split. contradiction. right ; rewrite H1 ; trivial. now left. contradiction. Qed.
imports: Coq(Reals ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy SF_seq RInt