proposition: Lemma Vn_growing : forall (Un:nat -> R) (pr:has_lb Un), Un_growing (sequence_lb Un pr).
proof: Proof. intros. unfold Un_growing. intro. unfold sequence_lb. assert (H := lb_to_glb (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr)). assert (H0 := lb_to_glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr)). elim H; intros. elim H0; intros. cut (glb (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr) = - x); [ intro Maj1; rewrite Maj1 | idtac ]. 1:cut (glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr) = - x0); [ intro Maj2; rewrite Maj2 | idtac ]. - unfold is_lub in p. unfold is_lub in p0. elim p; intros. apply Ropp_le_contravar. apply H2. elim p0; intros. unfold is_upper_bound. intros. unfold is_upper_bound in H3. apply H3. elim H5; intros. exists (1 + x2)%nat. unfold opp_seq in H6. unfold opp_seq. replace (n + (1 + x2))%nat with (S n + x2)%nat. + assumption. + replace (S n) with (1 + n)%nat; [ ring | ring ]. - cut (is_lub (EUn (opp_seq (fun k:nat => Un (n + k)%nat))) (- glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr))). + intro. unfold is_lub in p0; unfold is_lub in H1. elim p0; intros; elim H1; intros. assert (H6 := H5 x0 H2). assert (H7 := H3 (- glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr)) H4). rewrite <- (Ropp_involutive (glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr))) . apply Ropp_eq_compat; apply Rle_antisym; assumption. + unfold glb. case (lb_to_glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr)); simpl. intro; rewrite Ropp_involutive. trivial. - cut (is_lub (EUn (opp_seq (fun k:nat => Un (S n + k)%nat))) (- glb (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr))). + intro. unfold is_lub in p; unfold is_lub in H1. elim p; intros; elim H1; intros. assert (H6 := H5 x H2). assert (H7 := H3 (- glb (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr)) H4). rewrite <- (Ropp_involutive (glb (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr))) . apply Ropp_eq_compat; apply Rle_antisym; assumption. + unfold glb. case (lb_to_glb (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr)); simpl. intro; rewrite Ropp_involutive. trivial. Qed.
imports: Rbase Rfunctions Rseries Lia