proposition: Lemma ub_to_lub : forall Un:nat -> R, has_ub Un -> { l:R | is_lub (EUn Un) l }.
proof: Proof. intros. unfold has_ub in H. apply completeness. - assumption. - exists (Un 0%nat). unfold EUn. exists 0%nat; reflexivity. Qed.
imports: Rbase Rfunctions Rseries Lia