proposition: Lemma Vn_Un_Wn_order : forall (Un:nat -> R) (pr1:has_ub Un) (pr2:has_lb Un) (n:nat), sequence_lb Un pr2 n <= Un n <= sequence_ub Un pr1 n.
proof: Proof. intros. split. - unfold sequence_lb. cut { l:R | is_lub (EUn (opp_seq (fun i:nat => Un (n + i)%nat))) l }. + intro X. elim X; intros. replace (glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2)) with (- x). * unfold is_lub in p. elim p; intros. unfold is_upper_bound in H. rewrite <- (Ropp_involutive (Un n)). apply Ropp_le_contravar. apply H. exists 0%nat. unfold opp_seq. replace (n + 0)%nat with n; [ reflexivity | 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 pr2))). -- intro. unfold is_lub in p; unfold is_lub in H. elim p; intros; elim H; intros. assert (H4 := H3 x H0). assert (H5 := H1 (- glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2)) H2). rewrite <- (Ropp_involutive (glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2))) . 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 pr2)); simpl. intro; rewrite Ropp_involutive. trivial. + apply lb_to_glb. apply min_ss; assumption. - unfold sequence_ub. cut { l:R | is_lub (EUn (fun i:nat => Un (n + i)%nat)) l }. + intro X. elim X; intros. replace (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr1)) with x. * unfold is_lub in p. elim p; intros. unfold is_upper_bound in H. apply H. exists 0%nat. replace (n + 0)%nat with n; [ reflexivity | ring ]. * cut (is_lub (EUn (fun k:nat => Un (n + k)%nat)) (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr1))). -- intro. unfold is_lub in p; unfold is_lub in H. elim p; intros; elim H; intros. assert (H4 := H3 x H0). assert (H5 := H1 (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr1)) H2). apply Rle_antisym; assumption. -- unfold lub. case (ub_to_lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr1)). intro; trivial. + apply ub_to_lub. apply maj_ss; assumption. Qed.
imports: Rbase Rfunctions Rseries Lia