proposition: Lemma min_maj : forall (Un:nat -> R) (pr1:has_ub Un) (pr2:has_lb Un), has_ub (sequence_lb Un pr2).
proof: Proof. intros. assert (H := Vn_Un_Wn_order Un pr1 pr2). unfold has_ub. unfold bound. unfold has_ub in pr1. unfold bound in pr1. elim pr1; intros. exists x. unfold is_upper_bound. intros. unfold is_upper_bound in H0. elim H1; intros. rewrite H2. apply Rle_trans with (Un x1). - assert (H3 := H x1); elim H3; intros; assumption. - apply H0. exists x1; reflexivity. Qed.
imports: Rbase Rfunctions Rseries Lia