proposition: Lemma archimed_cor1 : forall eps:R, 0 < eps -> exists N : nat, / INR N < eps /\ (0 < N)%nat.
proof: Proof. intros; assert (/ eps < IZR (up (/ eps))). { assert (H0 := archimed (/ eps)). elim H0; intros; assumption. } assert (0 <= up (/ eps))%Z. { apply le_IZR; left; apply Rlt_trans with (/ eps); [ apply Rinv_0_lt_compat; assumption | assumption ]. } assert (H2 := IZN _ H1); elim H2; intros; exists (max x 1). split. - assert (0 < IZR (Z.of_nat x)). { apply Rlt_trans with (/ eps). - apply Rinv_0_lt_compat; assumption. - rewrite H3 in H0; assumption. } rewrite INR_IZR_INZ; apply Rle_lt_trans with (/ IZR (Z.of_nat x)). + apply Rmult_le_reg_l with (IZR (Z.of_nat x)). { assumption. } rewrite Rinv_r; [ idtac | red; intro; rewrite H5 in H4; elim (Rlt_irrefl _ H4) ]. apply Rmult_le_reg_l with (IZR (Z.of_nat (max x 1))). * apply Rlt_le_trans with (IZR (Z.of_nat x)). -- assumption. -- repeat rewrite <- INR_IZR_INZ; apply le_INR; apply Nat.le_max_l. * rewrite Rmult_1_r; rewrite (Rmult_comm (IZR (Z.of_nat (max x 1)))); rewrite Rmult_assoc; rewrite Rinv_l. -- rewrite Rmult_1_r; repeat rewrite <- INR_IZR_INZ; apply le_INR; apply Nat.le_max_l. -- rewrite <- INR_IZR_INZ; apply not_O_INR. red; intro; assert (H6 := Nat.le_max_r x 1); cut (0 < 1)%nat; [ intro | apply Nat.lt_0_succ ]; assert (H8 := Nat.lt_le_trans _ _ _ H7 H6); rewrite H5 in H8; elim (Nat.lt_irrefl _ H8). + pattern eps at 1; rewrite <- Rinv_inv. apply Rinv_lt_contravar. * apply Rmult_lt_0_compat; [ apply Rinv_0_lt_compat; assumption | assumption ]. * rewrite H3 in H0; assumption. - apply Nat.lt_le_trans with 1%nat; [ apply Nat.lt_0_succ | apply Nat.le_max_r ]. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_fun Lra Lia