proposition: Lemma sup_tail_is_Cauchy : Cauchy_prop (fun m : nat => sup_tail m).
proof: Proof. red in |- *. intros. cut {N : nat | forall m : nat, N <= m -> AbsSmall (e [/]TwoNZ) (g_ m[-]g_ N)}. intros H0. case H0. intro N. intros. exists N. intros. split. apply inv_cancel_leEq. rstepl (sup_tail N[-]sup_tail m). rstepr e. rewrite -> leEq_def; intro. apply (less_irreflexive_unfolded _ e). case (Psup_unfolded2 (tail_seq g N) (sup_tail m[+]e)). change (sup_tail m[+]e[<]sup_tail N) in |- *. apply shift_plus_less'. assumption. intro xj. intros H4 H5. red in H4. case H4. intro j. intros. apply less_leEq_trans with (y := g_ (N + j)[-]g_ m). apply shift_less_minus. apply shift_plus_less'. apply leEq_less_trans with (y := sup_tail m). apply sup_tail_leEq. apply le_n. apply shift_less_minus. apply less_wdr with (y := xj). assumption. assumption. cut (AbsSmall e (g_ (N + j)[-]g_ m)). intro H7. elim H7. intros H8 H9. assumption. rstepr (g_ (N + j)[-]g_ N[+](g_ N[-]g_ m)). rstepl (e [/]TwoNZ[+]e [/]TwoNZ). apply AbsSmall_plus. apply a. apply Nat.le_add_r. apply AbsSmall_minus. apply a. assumption. apply less_leEq. apply leEq_less_trans with (y := e [/]TwoNZ). rewrite -> leEq_def. intro. apply (less_irreflexive_unfolded _ (e [/]TwoNZ)). case (Psup_unfolded2 (tail_seq g m) (sup_tail N[+]e [/]TwoNZ)). change (sup_tail N[+]e [/]TwoNZ[<]sup_tail m) in |- *. apply shift_plus_less'. assumption. intro xj. intros H4 H5. red in H4. case H4. intro j. intros. apply less_leEq_trans with (y := g_ (m + j)[-]g_ N). apply shift_less_minus. apply shift_plus_less'. apply leEq_less_trans with (y := sup_tail N). apply sup_tail_leEq. apply le_n. apply shift_less_minus. apply less_wdr with (y := xj). assumption. assumption. cut (AbsSmall (e [/]TwoNZ) (g_ (m + j)[-]g_ N)). intro H7. elim H7. intros. assumption. apply a. apply Nat.le_trans with (m := m). assumption. apply Nat.le_add_r. apply pos_div_two'. assumption. apply pg. apply pos_div_two. assumption. Qed.
imports: CoRN.reals.Bridges_LUB