proposition: Lemma Un_bound_imp : forall x:R, (forall n:nat, Un n <= x) -> is_upper_bound EUn x.
proof: Proof. intros; unfold is_upper_bound; intros; unfold EUn in H0; elim H0; clear H0; intros; generalize (H x1); intro; rewrite <- H0 in H1; trivial. Qed.
imports: Rbase Rfunctions Compare