proposition: Lemma Wn_decreasing : forall (Un:nat -> R) (pr:has_ub Un), Un_decreasing (sequence_ub Un pr).
proof: Proof. intros. unfold Un_decreasing. intro. unfold sequence_ub. pose proof (ub_to_lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)) as (x,(H1,H2)). pose proof (ub_to_lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)) as (x0,(H3,H4)). cut (lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr) = x); [ intro Maj1; rewrite Maj1 | idtac ]. 1:cut (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr) = x0); [ intro Maj2; rewrite Maj2 | idtac ]. - apply H2. unfold is_upper_bound. intros x1 H5. unfold is_upper_bound in H3. apply H3. elim H5; intros. exists (1 + x2)%nat. replace (n + (1 + x2))%nat with (S n + x2)%nat. + assumption. + replace (S n) with (1 + n)%nat; [ ring | ring ]. - cut (is_lub (EUn (fun k:nat => Un (n + k)%nat)) (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr))). + intros (H5,H6). assert (H7 := H6 x0 H3). assert (H8 := H4 (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)) H5). apply Rle_antisym; assumption. + unfold lub. case (ub_to_lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)). trivial. - cut (is_lub (EUn (fun k:nat => Un (S n + k)%nat)) (lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr))). + intros (H5,H6). assert (H7 := H6 x H1). assert (H8 := H2 (lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)) H5). apply Rle_antisym; assumption. + unfold lub. case (ub_to_lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)). trivial. Qed.
imports: Rbase Rfunctions Rseries Lia