proposition: Lemma Cnested_intervals_limit : {z : IR | forall i, a i [<=] z | forall i, z [<=] b i}.
proof: Proof. exists (Lim a'). intros. rewrite -> leEq_def in |- *. unfold Not in |- *. intros. elim (Lim_less_so_seq_less a' (a i)). intro n. intros H0. elim (le_lt_dec n i); intro H1. cut (Not (a i [<] a i)). intro H2. unfold Not in H1. elim H2. apply H0. auto. apply less_irreflexive_unfolded. cut (forall i j : nat, i <= j -> a i [<=] a j). intro a_mon''. pose (c:=a_mon'' i n). rewrite -> leEq_def in c. apply c. auto with arith. apply H0. auto. intros. apply a_mon'; auto. auto. intros i. rewrite -> leEq_def. unfold Not. intros H. elim (less_Lim_so_less_seq a' (b i) H). intro n. intros H0. elim (le_lt_dec n i); intro H1. cut (Not (a i [<] b i)). unfold Not in |- *. intro. elim H2. auto. apply less_antisymmetric_unfolded. apply H0. auto. cut (Not (a n [<] b n)). unfold Not in |- *. intro H2. apply H2. auto. apply less_antisymmetric_unfolded. apply leEq_less_trans with (b i). apply b_mon'. auto with arith. apply H0. auto. Qed.
imports: CoRN.reals.CPoly_Contin