proposition: Lemma tail_is_Cauchy : forall n : nat, Cauchy_prop (fun m : nat => g_ (n + m)).
proof: Proof. intros. red in |- *. intros. case (pg (e [/]TwoNZ)). apply pos_div_two. assumption. intro N. intros. exists N. intros. rstepr (g_ (n + m)[-]g_ N[+](g_ N[-]g_ (n + N))). rstepl (e [/]TwoNZ[+]e [/]TwoNZ). apply AbsSmall_plus. apply a. apply Nat.le_trans with (m := m). assumption. rewrite Nat.add_comm; apply Nat.le_add_r. apply AbsSmall_minus. apply a. rewrite Nat.add_comm; apply Nat.le_add_r. Qed.
imports: CoRN.reals.Bridges_LUB