proposition: Lemma is_lub_u : forall (E:R -> Prop) (x y:R), is_lub E x -> is_lub E y -> x = y.
proof: Proof. unfold is_lub; intros; elim H; elim H0; intros; apply Rle_antisym; [ apply (H4 _ H1) | apply (H2 _ H3) ]. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type