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