proposition: Lemma cauchy_bound : Cauchy_crit -> bound EUn.
proof: Proof. unfold Cauchy_crit, bound; intros; unfold is_upper_bound; unfold Rgt in H; elim (H 1 Rlt_0_1); clear H; intros; generalize (H x); intro; generalize (le_dec x); intro; elim (finite_greater x); intros; split with (Rmax x0 (Un x + 1)); clear H; intros; unfold EUn in H; elim H; clear H; intros; elim (H1 x2); clear H1; intro y. - unfold ge in H0; generalize (H0 x2 (le_n x) y); clear H0; intro; rewrite <- H in H0; unfold Rdist in H0; elim (Rabs_def2 (Un x - x1) 1 H0); clear H0; intros; elim (Rmax_Rle x0 (Un x + 1) x1); intros; apply H4; clear H3 H4; right; clear H H0 y; apply (Rlt_le x1 (Un x + 1)); generalize (Rlt_minus (-1) (Un x - x1) H1); clear H1; intro; apply (Rminus_lt x1 (Un x + 1)); cut (-1 - (Un x - x1) = x1 - (Un x + 1)); [ intro; rewrite H0 in H; assumption | ring ]. - generalize (H2 x2 y); clear H2 H0; intro; rewrite <- H in H0; elim (Rmax_Rle x0 (Un x + 1) x1); intros; clear H1; apply H2; left; assumption. Qed.
imports: Rbase Rfunctions Compare