Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import Rbase Rfunctions SeqSeries Rtrigo_fun Max.
Local Open Scope R_scope.

(********************************)

Definition of exponential

(********************************)
Definition exp_in (x l:R) : Prop :=
  infinite_sum (fun i:nat => / INR (fact i) * x ^ i) l.

Lemma exp_cof_no_R0 : forall n:nat, / INR (fact n) <> 0.forall n : nat, / INR (fact n) <> 0
Proof.forall n : nat, / INR (fact n) <> 0
  intro.n:nat
/ INR (fact n) <> 0
  apply Rinv_neq_0_compat.n:nat
INR (fact n) <> 0
  apply INR_fact_neq_0.
Qed.

Lemma exist_exp : forall x:R, { l:R | exp_in x l }.forall x : R, {l : R | exp_in x l}
Proof.forall x : R, {l : R | exp_in x l}
  intro;
    generalize
      (Alembert_C3 (fun n:nat => / INR (fact n)) x exp_cof_no_R0 Alembert_exp).x:R
{l : R | Pser (fun n : nat => / INR (fact n)) x l} ->
{l : R | exp_in x l}
  unfold Pser, exp_in.x:R
{l : R |
infinite_sum (fun n : nat => / INR (fact n) * x ^ n) l} ->
{l : R |
infinite_sum (fun i : nat => / INR (fact i) * x ^ i) l}
  trivial.
Defined.

Definition exp (x:R) : R := proj1_sig (exist_exp x).

Lemma pow_i : forall i:nat, (0 < i)%nat -> 0 ^ i = 0.forall i : nat, (0 < i)%nat -> 0 ^ i = 0
Proof.forall i : nat, (0 < i)%nat -> 0 ^ i = 0
  intros; apply pow_ne_zero.i:nat
H:(0 < i)%nat
i <> 0%nat
  red; intro; rewrite H0 in H; elim (lt_irrefl _ H).
Qed.

Lemma exist_exp0 : { l:R | exp_in 0 l }.{l : R | exp_in 0 l}
Proof.{l : R | exp_in 0 l}
  exists 1.exp_in 0 1
  unfold exp_in; unfold infinite_sum; intros.eps:R
H:eps > 0
exists N : nat,
  forall n : nat,
  (n >= N)%nat ->
  R_dist
    (sum_f_R0 (fun i : nat => / INR (fact i) * 0 ^ i)
       n) 1 < eps
  exists 0%nat.eps:R
H:eps > 0
forall n : nat,
(n >= 0)%nat ->
R_dist
  (sum_f_R0 (fun i : nat => / INR (fact i) * 0 ^ i) n)
  1 < eps
  intros; replace (sum_f_R0 (fun i:nat => / INR (fact i) * 0 ^ i) n) with 1.eps:R
H:eps > 0
n:nat
H0:(n >= 0)%nat
R_dist 1 1 < eps
eps:R
H:eps > 0
n:nat
H0:(n >= 0)%nat
1 = sum_f_R0 (fun i : nat => / INR (fact i) * 0 ^ i) n
  unfold R_dist; replace (1 - 1) with 0;
    [ rewrite Rabs_R0; assumption | ring ].eps:R
H:eps > 0
n:nat
H0:(n >= 0)%nat
1 = sum_f_R0 (fun i : nat => / INR (fact i) * 0 ^ i) n
  induction  n as [| n Hrecn].eps:R
H:eps > 0
H0:(0 >= 0)%nat
1 = sum_f_R0 (fun i : nat => / INR (fact i) * 0 ^ i) 0
eps:R
H:eps > 0
n:nat
H0:(S n >= 0)%nat
Hrecn:(n >= 0)%nat ->
1 =
sum_f_R0
  (fun i : nat => / INR (fact i) * 0 ^ i) n
1 =
sum_f_R0 (fun i : nat => / INR (fact i) * 0 ^ i) (S n)
  simpl; rewrite Rinv_1; ring.eps:R
H:eps > 0
n:nat
H0:(S n >= 0)%nat
Hrecn:(n >= 0)%nat ->
1 =
sum_f_R0
  (fun i : nat => / INR (fact i) * 0 ^ i) n
1 =
sum_f_R0 (fun i : nat => / INR (fact i) * 0 ^ i) (S n)
  rewrite tech5.eps:R
H:eps > 0
n:nat
H0:(S n >= 0)%nat
Hrecn:(n >= 0)%nat ->
1 =
sum_f_R0
  (fun i : nat => / INR (fact i) * 0 ^ i) n
1 =
sum_f_R0 (fun i : nat => / INR (fact i) * 0 ^ i) n +
/ INR (fact (S n)) * 0 ^ S n
  rewrite <- Hrecn.eps:R
H:eps > 0
n:nat
H0:(S n >= 0)%nat
Hrecn:(n >= 0)%nat ->
1 =
sum_f_R0
  (fun i : nat => / INR (fact i) * 0 ^ i) n
1 = 1 + / INR (fact (S n)) * 0 ^ S n
eps:R
H:eps > 0
n:nat
H0:(S n >= 0)%nat
Hrecn:(n >= 0)%nat ->
1 =
sum_f_R0
  (fun i : nat => / INR (fact i) * 0 ^ i) n
(n >= 0)%nat
  simpl.eps:R
H:eps > 0
n:nat
H0:(S n >= 0)%nat
Hrecn:(n >= 0)%nat ->
1 =
sum_f_R0
  (fun i : nat => / INR (fact i) * 0 ^ i) n
1 = 1 + / INR (fact n + n * fact n) * (0 * 0 ^ n)
eps:R
H:eps > 0
n:nat
H0:(S n >= 0)%nat
Hrecn:(n >= 0)%nat ->
1 =
sum_f_R0
  (fun i : nat => / INR (fact i) * 0 ^ i) n
(n >= 0)%nat
  ring.eps:R
H:eps > 0
n:nat
H0:(S n >= 0)%nat
Hrecn:(n >= 0)%nat ->
1 =
sum_f_R0
  (fun i : nat => / INR (fact i) * 0 ^ i) n
(n >= 0)%nat
  unfold ge; apply le_O_n.
Defined.

(* Value of [exp 0] *)
Lemma exp_0 : exp 0 = 1.exp 0 = 1
Proof.exp 0 = 1
  cut (exp_in 0 (exp 0)).exp_in 0 (exp 0) -> exp 0 = 1
exp_in 0 (exp 0)
  cut (exp_in 0 1).exp_in 0 1 -> exp_in 0 (exp 0) -> exp 0 = 1
exp_in 0 1
exp_in 0 (exp 0)
  unfold exp_in; intros; eapply uniqueness_sum.H:infinite_sum
  (fun i : nat => / INR (fact i) * 0 ^ i) 1
H0:infinite_sum
  (fun i : nat => / INR (fact i) * 0 ^ i) (exp 0)
infinite_sum ?An (exp 0)
H:infinite_sum
  (fun i : nat => / INR (fact i) * 0 ^ i) 1
H0:infinite_sum
  (fun i : nat => / INR (fact i) * 0 ^ i) (exp 0)
infinite_sum ?An 1
exp_in 0 1
exp_in 0 (exp 0)
  apply H0.H:infinite_sum
  (fun i : nat => / INR (fact i) * 0 ^ i) 1
H0:infinite_sum
  (fun i : nat => / INR (fact i) * 0 ^ i) (exp 0)
infinite_sum (fun i : nat => / INR (fact i) * 0 ^ i) 1
exp_in 0 1
exp_in 0 (exp 0)
  apply H.exp_in 0 1
exp_in 0 (exp 0)
  exact (proj2_sig exist_exp0).exp_in 0 (exp 0)
  exact (proj2_sig (exist_exp 0)).
Qed.

(*****************************************)

Definition of hyperbolic functions

(*****************************************)
Definition cosh (x:R) : R := (exp x + exp (- x)) / 2.
Definition sinh (x:R) : R := (exp x - exp (- x)) / 2.
Definition tanh (x:R) : R := sinh x / cosh x.

Lemma cosh_0 : cosh 0 = 1.cosh 0 = 1
Proof.cosh 0 = 1
  unfold cosh; rewrite Ropp_0; rewrite exp_0.(1 + 1) / 2 = 1
  unfold Rdiv; rewrite <- Rinv_r_sym; [ reflexivity | discrR ].
Qed.

Lemma sinh_0 : sinh 0 = 0.sinh 0 = 0
Proof.sinh 0 = 0
  unfold sinh; rewrite Ropp_0; rewrite exp_0.(1 - 1) / 2 = 0
  unfold Rminus, Rdiv; rewrite Rplus_opp_r; apply Rmult_0_l.
Qed.

Definition cos_n (n:nat) : R := (-1) ^ n / INR (fact (2 * n)).

Lemma simpl_cos_n :
  forall n:nat, cos_n (S n) / cos_n n = - / INR (2 * S n * (2 * n + 1)).forall n : nat,
cos_n (S n) / cos_n n =
- / INR (2 * S n * (2 * n + 1))
Proof.forall n : nat,
cos_n (S n) / cos_n n =
- / INR (2 * S n * (2 * n + 1))
  intro; unfold cos_n; replace (S n) with (n + 1)%nat; [ idtac | ring ].n:nat
(-1) ^ (n + 1) / INR (fact (2 * (n + 1))) /
((-1) ^ n / INR (fact (2 * n))) =
- / INR (2 * (n + 1) * (2 * n + 1))
  rewrite pow_add; unfold Rdiv; rewrite Rinv_mult_distr.n:nat
(-1) ^ n * (-1) ^ 1 * / INR (fact (2 * (n + 1))) *
(/ (-1) ^ n * / / INR (fact (2 * n))) =
- / INR (2 * (n + 1) * (2 * n + 1))
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n)) <> 0
  rewrite Rinv_involutive.n:nat
(-1) ^ n * (-1) ^ 1 * / INR (fact (2 * (n + 1))) *
(/ (-1) ^ n * INR (fact (2 * n))) =
- / INR (2 * (n + 1) * (2 * n + 1))
n:nat
INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n)) <> 0
  replace
  ((-1) ^ n * (-1) ^ 1 * / INR (fact (2 * (n + 1))) *
    (/ (-1) ^ n * INR (fact (2 * n)))) with
  ((-1) ^ n * / (-1) ^ n * / INR (fact (2 * (n + 1))) * INR (fact (2 * n)) *
    (-1) ^ 1); [ idtac | ring ].n:nat
(-1) ^ n * / (-1) ^ n * / INR (fact (2 * (n + 1))) *
INR (fact (2 * n)) * (-1) ^ 1 =
- / INR (2 * (n + 1) * (2 * n + 1))
n:nat
INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n)) <> 0
  rewrite <- Rinv_r_sym.n:nat
1 * / INR (fact (2 * (n + 1))) * INR (fact (2 * n)) *
(-1) ^ 1 = - / INR (2 * (n + 1) * (2 * n + 1))
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n)) <> 0
  rewrite Rmult_1_l; unfold pow; rewrite Rmult_1_r.n:nat
/ INR (fact (2 * (n + 1))) * INR (fact (2 * n)) * -1 =
- / INR (2 * (n + 1) * (2 * n + 1))
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n)) <> 0
  replace (2 * (n + 1))%nat with (S (S (2 * n))); [ idtac | ring ].n:nat
/ INR (fact (S (S (2 * n)))) * INR (fact (2 * n)) * -1 =
- / INR (S (S (2 * n)) * (2 * n + 1))
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n)) <> 0
  do 2 rewrite fact_simpl; do 2 rewrite mult_INR;
    repeat rewrite Rinv_mult_distr; try (apply not_O_INR; discriminate).n:nat
/ INR (S (S (2 * n))) *
(/ INR (S (2 * n)) * / INR (fact (2 * n))) *
INR (fact (2 * n)) * -1 =
- / INR (S (S (2 * n)) * (2 * n + 1))
n:nat
INR (fact (2 * n)) <> 0
n:nat
INR (S (2 * n)) * INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n)) <> 0
  rewrite <- (Rmult_comm (-1)).n:nat
-1 *
(/ INR (S (S (2 * n))) *
 (/ INR (S (2 * n)) * / INR (fact (2 * n))) *
 INR (fact (2 * n))) =
- / INR (S (S (2 * n)) * (2 * n + 1))
n:nat
INR (fact (2 * n)) <> 0
n:nat
INR (S (2 * n)) * INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n)) <> 0
  repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.n:nat
-1 * (/ INR (S (S (2 * n))) * (/ INR (S (2 * n)) * 1)) =
- / INR (S (S (2 * n)) * (2 * n + 1))
n:nat
INR (fact (2 * n)) <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
INR (S (2 * n)) * INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n)) <> 0
  rewrite Rmult_1_r.n:nat
-1 * (/ INR (S (S (2 * n))) * / INR (S (2 * n))) =
- / INR (S (S (2 * n)) * (2 * n + 1))
n:nat
INR (fact (2 * n)) <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
INR (S (2 * n)) * INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n)) <> 0
  replace (S (2 * n)) with (2 * n + 1)%nat; [ idtac | ring ].n:nat
-1 * (/ INR (S (2 * n + 1)) * / INR (2 * n + 1)) =
- / INR (S (2 * n + 1) * (2 * n + 1))
n:nat
INR (fact (2 * n)) <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
INR (S (2 * n)) * INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n)) <> 0
  rewrite mult_INR; rewrite Rinv_mult_distr.n:nat
-1 * (/ INR (S (2 * n + 1)) * / INR (2 * n + 1)) =
- (/ INR (S (2 * n + 1)) * / INR (2 * n + 1))
n:nat
INR (S (2 * n + 1)) <> 0
n:nat
INR (2 * n + 1) <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
INR (S (2 * n)) * INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n)) <> 0
  ring.n:nat
INR (S (2 * n + 1)) <> 0
n:nat
INR (2 * n + 1) <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
INR (S (2 * n)) * INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n)) <> 0
  apply not_O_INR; discriminate.n:nat
INR (2 * n + 1) <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
INR (S (2 * n)) * INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n)) <> 0
  replace (2 * n + 1)%nat with (S (2 * n));
  [ apply not_O_INR; discriminate | ring ].n:nat
INR (fact (2 * n)) <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
INR (S (2 * n)) * INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n)) <> 0
  apply INR_fact_neq_0.n:nat
INR (fact (2 * n)) <> 0
n:nat
INR (S (2 * n)) * INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n)) <> 0
  apply INR_fact_neq_0.n:nat
INR (S (2 * n)) * INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n)) <> 0
  apply prod_neq_R0; [ apply not_O_INR; discriminate | apply INR_fact_neq_0 ].n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n)) <> 0
  apply pow_nonzero; discrR.n:nat
INR (fact (2 * n)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n)) <> 0
  apply INR_fact_neq_0.n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n)) <> 0
  apply pow_nonzero; discrR.n:nat
/ INR (fact (2 * n)) <> 0
  apply Rinv_neq_0_compat; apply INR_fact_neq_0.
Qed.

Lemma archimed_cor1 :
  forall eps:R, 0 < eps ->  exists N : nat, / INR N < eps /\ (0 < N)%nat.forall eps : R,
0 < eps ->
exists N : nat, / INR N < eps /\ (0 < N)%nat
Proof.forall eps : R,
0 < eps ->
exists N : nat, / INR N < eps /\ (0 < N)%nat
  intros; cut (/ eps < IZR (up (/ eps))).eps:R
H:0 < eps
/ eps < IZR (up (/ eps)) ->
exists N : nat, / INR N < eps /\ (0 < N)%nat
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  intro; cut (0 <= up (/ eps))%Z.eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z ->
exists N : nat, / INR N < eps /\ (0 < N)%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  intro; assert (H2 := IZN _ H1); elim H2; intros; exists (max x 1).eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
/ INR (Nat.max x 1) < eps /\ (0 < Nat.max x 1)%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  split.eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
/ INR (Nat.max x 1) < eps
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
(0 < Nat.max x 1)%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  cut (0 < IZR (Z.of_nat x)).eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
0 < IZR (Z.of_nat x) -> / INR (Nat.max x 1) < eps
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
0 < IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
(0 < Nat.max x 1)%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  intro; rewrite INR_IZR_INZ; apply Rle_lt_trans with (/ IZR (Z.of_nat x)).eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
/ IZR (Z.of_nat (Nat.max x 1)) <= / IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
/ IZR (Z.of_nat x) < eps
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
0 < IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
(0 < Nat.max x 1)%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  apply Rmult_le_reg_l with (IZR (Z.of_nat x)).eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
0 < IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
IZR (Z.of_nat x) * / IZR (Z.of_nat (Nat.max x 1)) <=
IZR (Z.of_nat x) * / IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
/ IZR (Z.of_nat x) < eps
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
0 < IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
(0 < Nat.max x 1)%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  assumption.eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
IZR (Z.of_nat x) * / IZR (Z.of_nat (Nat.max x 1)) <=
IZR (Z.of_nat x) * / IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
/ IZR (Z.of_nat x) < eps
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
0 < IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
(0 < Nat.max x 1)%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  rewrite <- Rinv_r_sym;
    [ idtac | red; intro; rewrite H5 in H4; elim (Rlt_irrefl _ H4) ].eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
IZR (Z.of_nat x) * / IZR (Z.of_nat (Nat.max x 1)) <= 1
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
/ IZR (Z.of_nat x) < eps
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
0 < IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
(0 < Nat.max x 1)%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  apply Rmult_le_reg_l with (IZR (Z.of_nat (max x 1))).eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
0 < IZR (Z.of_nat (Nat.max x 1))
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
IZR (Z.of_nat (Nat.max x 1)) *
(IZR (Z.of_nat x) * / IZR (Z.of_nat (Nat.max x 1))) <=
IZR (Z.of_nat (Nat.max x 1)) * 1
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
/ IZR (Z.of_nat x) < eps
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
0 < IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
(0 < Nat.max x 1)%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  apply Rlt_le_trans with (IZR (Z.of_nat x)).eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
0 < IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
IZR (Z.of_nat x) <= IZR (Z.of_nat (Nat.max x 1))
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
IZR (Z.of_nat (Nat.max x 1)) *
(IZR (Z.of_nat x) * / IZR (Z.of_nat (Nat.max x 1))) <=
IZR (Z.of_nat (Nat.max x 1)) * 1
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
/ IZR (Z.of_nat x) < eps
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
0 < IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
(0 < Nat.max x 1)%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  assumption.eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
IZR (Z.of_nat x) <= IZR (Z.of_nat (Nat.max x 1))
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
IZR (Z.of_nat (Nat.max x 1)) *
(IZR (Z.of_nat x) * / IZR (Z.of_nat (Nat.max x 1))) <=
IZR (Z.of_nat (Nat.max x 1)) * 1
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
/ IZR (Z.of_nat x) < eps
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
0 < IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
(0 < Nat.max x 1)%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  repeat rewrite <- INR_IZR_INZ; apply le_INR; apply le_max_l.eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
IZR (Z.of_nat (Nat.max x 1)) *
(IZR (Z.of_nat x) * / IZR (Z.of_nat (Nat.max x 1))) <=
IZR (Z.of_nat (Nat.max x 1)) * 1
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
/ IZR (Z.of_nat x) < eps
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
0 < IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
(0 < Nat.max x 1)%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  rewrite Rmult_1_r; rewrite (Rmult_comm (IZR (Z.of_nat (max x 1))));
    rewrite Rmult_assoc; rewrite <- Rinv_l_sym.eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
IZR (Z.of_nat x) * 1 <= IZR (Z.of_nat (Nat.max x 1))
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
IZR (Z.of_nat (Nat.max x 1)) <> 0
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
/ IZR (Z.of_nat x) < eps
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
0 < IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
(0 < Nat.max x 1)%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  rewrite Rmult_1_r; repeat rewrite <- INR_IZR_INZ; apply le_INR;
    apply le_max_l.eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
IZR (Z.of_nat (Nat.max x 1)) <> 0
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
/ IZR (Z.of_nat x) < eps
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
0 < IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
(0 < Nat.max x 1)%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  rewrite <- INR_IZR_INZ; apply not_O_INR.eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
Nat.max x 1 <> 0%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
/ IZR (Z.of_nat x) < eps
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
0 < IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
(0 < Nat.max x 1)%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  red; intro; assert (H6 := le_max_r x 1); cut (0 < 1)%nat;
    [ intro | apply lt_O_Sn ]; assert (H8 := lt_le_trans _ _ _ H7 H6);
      rewrite H5 in H8; elim (lt_irrefl _ H8).eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
/ IZR (Z.of_nat x) < eps
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
0 < IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
(0 < Nat.max x 1)%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  pattern eps at 1; rewrite <- Rinv_involutive.eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
/ IZR (Z.of_nat x) < / / eps
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
eps <> 0
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
0 < IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
(0 < Nat.max x 1)%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  apply Rinv_lt_contravar.eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
0 < / eps * IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
/ eps < IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
eps <> 0
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
0 < IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
(0 < Nat.max x 1)%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  apply Rmult_lt_0_compat; [ apply Rinv_0_lt_compat; assumption | assumption ].eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
/ eps < IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
eps <> 0
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
0 < IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
(0 < Nat.max x 1)%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  rewrite H3 in H0; assumption.eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
H4:0 < IZR (Z.of_nat x)
eps <> 0
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
0 < IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
(0 < Nat.max x 1)%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  red; intro; rewrite H5 in H; elim (Rlt_irrefl _ H).eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
0 < IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
(0 < Nat.max x 1)%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  apply Rlt_trans with (/ eps).eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
0 < / eps
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
/ eps < IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
(0 < Nat.max x 1)%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  apply Rinv_0_lt_compat; assumption.eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
/ eps < IZR (Z.of_nat x)
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
(0 < Nat.max x 1)%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  rewrite H3 in H0; assumption.eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
H1:(0 <= up (/ eps))%Z
H2:exists m : nat, up (/ eps) = Z.of_nat m
x:nat
H3:up (/ eps) = Z.of_nat x
(0 < Nat.max x 1)%nat
eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  apply lt_le_trans with 1%nat; [ apply lt_O_Sn | apply le_max_r ].eps:R
H:0 < eps
H0:/ eps < IZR (up (/ eps))
(0 <= up (/ eps))%Z
eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  apply le_IZR; left;
    apply Rlt_trans with (/ eps);
      [ apply Rinv_0_lt_compat; assumption | assumption ].eps:R
H:0 < eps
/ eps < IZR (up (/ eps))
  assert (H0 := archimed (/ eps)).eps:R
H:0 < eps
H0:IZR (up (/ eps)) > / eps /\
IZR (up (/ eps)) - / eps <= 1
/ eps < IZR (up (/ eps))
  elim H0; intros; assumption.
Qed.

Lemma Alembert_cos : Un_cv (fun n:nat => Rabs (cos_n (S n) / cos_n n)) 0.Un_cv (fun n : nat => Rabs (cos_n (S n) / cos_n n)) 0
Proof.Un_cv (fun n : nat => Rabs (cos_n (S n) / cos_n n)) 0
  unfold Un_cv; intros.eps:R
H:eps > 0
exists N : nat,
  forall n : nat,
  (n >= N)%nat ->
  R_dist (Rabs (cos_n (S n) / cos_n n)) 0 < eps
  assert (H0 := archimed_cor1 eps H).eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
exists N : nat,
  forall n : nat,
  (n >= N)%nat ->
  R_dist (Rabs (cos_n (S n) / cos_n n)) 0 < eps
  elim H0; intros; exists x.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
forall n : nat,
(n >= x)%nat ->
R_dist (Rabs (cos_n (S n) / cos_n n)) 0 < eps
  intros; rewrite simpl_cos_n; unfold R_dist; unfold Rminus;
    rewrite Ropp_0; rewrite Rplus_0_r; rewrite Rabs_Rabsolu;
      rewrite Rabs_Ropp; rewrite Rabs_right.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  rewrite mult_INR; rewrite Rinv_mult_distr.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) * / INR (2 * n + 1) < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  cut (/ INR (2 * S n) < 1).eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1 ->
/ INR (2 * S n) * / INR (2 * n + 1) < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  intro; cut (/ INR (2 * n + 1) < eps).eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
/ INR (2 * n + 1) < eps ->
/ INR (2 * S n) * / INR (2 * n + 1) < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
/ INR (2 * n + 1) < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  intro; rewrite <- (Rmult_1_l eps).eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:/ INR (2 * n + 1) < eps
/ INR (2 * S n) * / INR (2 * n + 1) < 1 * eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
/ INR (2 * n + 1) < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  apply Rmult_gt_0_lt_compat; try assumption.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:/ INR (2 * n + 1) < eps
/ INR (2 * n + 1) > 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:/ INR (2 * n + 1) < eps
1 > 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
/ INR (2 * n + 1) < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  change (0 < / INR (2 * n + 1)); apply Rinv_0_lt_compat;
    apply lt_INR_0.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:/ INR (2 * n + 1) < eps
(0 < 2 * n + 1)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:/ INR (2 * n + 1) < eps
1 > 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
/ INR (2 * n + 1) < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  replace (2 * n + 1)%nat with (S (2 * n)); [ apply lt_O_Sn | ring ].eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:/ INR (2 * n + 1) < eps
1 > 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
/ INR (2 * n + 1) < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  apply Rlt_0_1.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
/ INR (2 * n + 1) < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  cut (x < 2 * n + 1)%nat.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(x < 2 * n + 1)%nat -> / INR (2 * n + 1) < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(x < 2 * n + 1)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  intro; assert (H5 := lt_INR _ _ H4).eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * n + 1)%nat
H5:INR x < INR (2 * n + 1)
/ INR (2 * n + 1) < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(x < 2 * n + 1)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  apply Rlt_trans with (/ INR x).eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * n + 1)%nat
H5:INR x < INR (2 * n + 1)
/ INR (2 * n + 1) < / INR x
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * n + 1)%nat
H5:INR x < INR (2 * n + 1)
/ INR x < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(x < 2 * n + 1)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  apply Rinv_lt_contravar.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * n + 1)%nat
H5:INR x < INR (2 * n + 1)
0 < INR x * INR (2 * n + 1)
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * n + 1)%nat
H5:INR x < INR (2 * n + 1)
INR x < INR (2 * n + 1)
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * n + 1)%nat
H5:INR x < INR (2 * n + 1)
/ INR x < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(x < 2 * n + 1)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  apply Rmult_lt_0_compat.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * n + 1)%nat
H5:INR x < INR (2 * n + 1)
0 < INR x
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * n + 1)%nat
H5:INR x < INR (2 * n + 1)
0 < INR (2 * n + 1)
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * n + 1)%nat
H5:INR x < INR (2 * n + 1)
INR x < INR (2 * n + 1)
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * n + 1)%nat
H5:INR x < INR (2 * n + 1)
/ INR x < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(x < 2 * n + 1)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  apply lt_INR_0.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * n + 1)%nat
H5:INR x < INR (2 * n + 1)
(0 < x)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * n + 1)%nat
H5:INR x < INR (2 * n + 1)
0 < INR (2 * n + 1)
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * n + 1)%nat
H5:INR x < INR (2 * n + 1)
INR x < INR (2 * n + 1)
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * n + 1)%nat
H5:INR x < INR (2 * n + 1)
/ INR x < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(x < 2 * n + 1)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  elim H1; intros; assumption.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * n + 1)%nat
H5:INR x < INR (2 * n + 1)
0 < INR (2 * n + 1)
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * n + 1)%nat
H5:INR x < INR (2 * n + 1)
INR x < INR (2 * n + 1)
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * n + 1)%nat
H5:INR x < INR (2 * n + 1)
/ INR x < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(x < 2 * n + 1)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  apply lt_INR_0; replace (2 * n + 1)%nat with (S (2 * n));
    [ apply lt_O_Sn | ring ].eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * n + 1)%nat
H5:INR x < INR (2 * n + 1)
INR x < INR (2 * n + 1)
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * n + 1)%nat
H5:INR x < INR (2 * n + 1)
/ INR x < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(x < 2 * n + 1)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  assumption.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * n + 1)%nat
H5:INR x < INR (2 * n + 1)
/ INR x < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(x < 2 * n + 1)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  elim H1; intros; assumption.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(x < 2 * n + 1)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  apply lt_le_trans with (S n).eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(x < S n)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(S n <= 2 * n + 1)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  unfold ge in H2; apply le_lt_n_Sm; assumption.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(S n <= 2 * n + 1)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  replace (2 * n + 1)%nat with (S (2 * n)) by ring.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(S n <= S (2 * n))%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  apply le_n_S; apply le_n_2n.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  apply Rmult_lt_reg_l with (INR (2 * S n)).eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
0 < INR (2 * S n)
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) * / INR (2 * S n) < INR (2 * S n) * 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  apply lt_INR_0; replace (2 * S n)%nat with (S (S (2 * n))).eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
(0 < S (S (2 * n)))%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
S (S (2 * n)) = (2 * S n)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) * / INR (2 * S n) < INR (2 * S n) * 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  apply lt_O_Sn.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
S (S (2 * n)) = (2 * S n)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) * / INR (2 * S n) < INR (2 * S n) * 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  replace (S n) with (n + 1)%nat by ring.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
S (S (2 * n)) = (2 * (n + 1))%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) * / INR (2 * S n) < INR (2 * S n) * 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  ring.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) * / INR (2 * S n) < INR (2 * S n) * 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  rewrite <- Rinv_r_sym.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
1 < INR (2 * S n) * 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  rewrite Rmult_1_r.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
1 < INR (2 * S n)
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  apply (lt_INR 1).eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
(1 < 2 * S n)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  replace (2 * S n)%nat with (S (S (2 * n))).eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
(1 < S (S (2 * n)))%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
S (S (2 * n)) = (2 * S n)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  apply lt_n_S; apply lt_O_Sn.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
S (S (2 * n)) = (2 * S n)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  ring.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  apply not_O_INR; discriminate.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  apply not_O_INR; discriminate.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  replace (2 * n + 1)%nat with (S (2 * n));
  [ apply not_O_INR; discriminate | ring ].eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n * (2 * n + 1)) >= 0
  apply Rle_ge; left; apply Rinv_0_lt_compat.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
0 < INR (2 * S n * (2 * n + 1))
  apply lt_INR_0.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
(0 < 2 * S n * (2 * n + 1))%nat
  replace (2 * S n * (2 * n + 1))%nat with (2 + (4 * (n * n) + 6 * n))%nat by ring.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
(0 < 2 + (4 * (n * n) + 6 * n))%nat
  apply lt_O_Sn.
Qed.

Lemma cosn_no_R0 : forall n:nat, cos_n n <> 0.forall n : nat, cos_n n <> 0
Proof.forall n : nat, cos_n n <> 0
  intro; unfold cos_n; unfold Rdiv; apply prod_neq_R0.n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n)) <> 0
  apply pow_nonzero; discrR.n:nat
/ INR (fact (2 * n)) <> 0
  apply Rinv_neq_0_compat.n:nat
INR (fact (2 * n)) <> 0
  apply INR_fact_neq_0.
Qed.

(**********)
Definition cos_in (x l:R) : Prop :=
  infinite_sum (fun i:nat => cos_n i * x ^ i) l.

(**********)
Lemma exist_cos : forall x:R, { l:R | cos_in x l }.forall x : R, {l : R | cos_in x l}
Proof.forall x : R, {l : R | cos_in x l}
  intro; generalize (Alembert_C3 cos_n x cosn_no_R0 Alembert_cos).x:R
{l : R | Pser cos_n x l} -> {l : R | cos_in x l}
  unfold Pser, cos_in; trivial.
Qed.

Definition of cosinus

Definition cos (x:R) : R := let (a,_) := exist_cos (Rsqr x) in a.

Definition sin_n (n:nat) : R := (-1) ^ n / INR (fact (2 * n + 1)).

Lemma simpl_sin_n :
  forall n:nat, sin_n (S n) / sin_n n = - / INR ((2 * S n + 1) * (2 * S n)).forall n : nat,
sin_n (S n) / sin_n n =
- / INR ((2 * S n + 1) * (2 * S n))
Proof.forall n : nat,
sin_n (S n) / sin_n n =
- / INR ((2 * S n + 1) * (2 * S n))
  intro; unfold sin_n; replace (S n) with (n + 1)%nat; [ idtac | ring ].n:nat
(-1) ^ (n + 1) / INR (fact (2 * (n + 1) + 1)) /
((-1) ^ n / INR (fact (2 * n + 1))) =
- / INR ((2 * (n + 1) + 1) * (2 * (n + 1)))
  rewrite pow_add; unfold Rdiv; rewrite Rinv_mult_distr.n:nat
(-1) ^ n * (-1) ^ 1 * / INR (fact (2 * (n + 1) + 1)) *
(/ (-1) ^ n * / / INR (fact (2 * n + 1))) =
- / INR ((2 * (n + 1) + 1) * (2 * (n + 1)))
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  rewrite Rinv_involutive.n:nat
(-1) ^ n * (-1) ^ 1 * / INR (fact (2 * (n + 1) + 1)) *
(/ (-1) ^ n * INR (fact (2 * n + 1))) =
- / INR ((2 * (n + 1) + 1) * (2 * (n + 1)))
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  replace
  ((-1) ^ n * (-1) ^ 1 * / INR (fact (2 * (n + 1) + 1)) *
    (/ (-1) ^ n * INR (fact (2 * n + 1)))) with
  ((-1) ^ n * / (-1) ^ n * / INR (fact (2 * (n + 1) + 1)) *
    INR (fact (2 * n + 1)) * (-1) ^ 1); [ idtac | ring ].n:nat
(-1) ^ n * / (-1) ^ n * / INR (fact (2 * (n + 1) + 1)) *
INR (fact (2 * n + 1)) * (-1) ^ 1 =
- / INR ((2 * (n + 1) + 1) * (2 * (n + 1)))
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  rewrite <- Rinv_r_sym.n:nat
1 * / INR (fact (2 * (n + 1) + 1)) *
INR (fact (2 * n + 1)) * (-1) ^ 1 =
- / INR ((2 * (n + 1) + 1) * (2 * (n + 1)))
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  rewrite Rmult_1_l; unfold pow; rewrite Rmult_1_r;
    replace (2 * (n + 1) + 1)%nat with (S (S (2 * n + 1))).n:nat
/ INR (fact (S (S (2 * n + 1)))) *
INR (fact (2 * n + 1)) * -1 =
- / INR (S (S (2 * n + 1)) * (2 * (n + 1)))
n:nat
S (S (2 * n + 1)) = (2 * (n + 1) + 1)%nat
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  do 2 rewrite fact_simpl; do 2 rewrite mult_INR;
    repeat rewrite Rinv_mult_distr.n:nat
/ INR (S (S (2 * n + 1))) *
(/ INR (S (2 * n + 1)) * / INR (fact (2 * n + 1))) *
INR (fact (2 * n + 1)) * -1 =
- / INR (S (S (2 * n + 1)) * (2 * (n + 1)))
n:nat
INR (S (2 * n + 1)) <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (S (2 * n + 1))) <> 0
n:nat
INR (S (2 * n + 1)) * INR (fact (2 * n + 1)) <> 0
n:nat
S (S (2 * n + 1)) = (2 * (n + 1) + 1)%nat
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  rewrite <- (Rmult_comm (-1)); repeat rewrite Rmult_assoc;
    rewrite <- Rinv_l_sym.n:nat
-1 *
(/ INR (S (S (2 * n + 1))) *
 (/ INR (S (2 * n + 1)) * 1)) =
- / INR (S (S (2 * n + 1)) * (2 * (n + 1)))
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (2 * n + 1)) <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (S (2 * n + 1))) <> 0
n:nat
INR (S (2 * n + 1)) * INR (fact (2 * n + 1)) <> 0
n:nat
S (S (2 * n + 1)) = (2 * (n + 1) + 1)%nat
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  rewrite Rmult_1_r; replace (S (2 * n + 1)) with (2 * (n + 1))%nat.n:nat
-1 * (/ INR (S (2 * (n + 1))) * / INR (2 * (n + 1))) =
- / INR (S (2 * (n + 1)) * (2 * (n + 1)))
n:nat
(2 * (n + 1))%nat = S (2 * n + 1)
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (2 * n + 1)) <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (S (2 * n + 1))) <> 0
n:nat
INR (S (2 * n + 1)) * INR (fact (2 * n + 1)) <> 0
n:nat
S (S (2 * n + 1)) = (2 * (n + 1) + 1)%nat
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  repeat rewrite mult_INR; repeat rewrite Rinv_mult_distr.n:nat
-1 *
(/ INR (S (2 * (n + 1))) * (/ INR 2 * / INR (n + 1))) =
-
(/ INR (S (2 * (n + 1))) * (/ INR 2 * / INR (n + 1)))
n:nat
INR 2 <> 0
n:nat
INR (n + 1) <> 0
n:nat
INR (S (2 * (n + 1))) <> 0
n:nat
INR 2 * INR (n + 1) <> 0
n:nat
INR 2 <> 0
n:nat
INR (n + 1) <> 0
n:nat
(2 * (n + 1))%nat = S (2 * n + 1)
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (2 * n + 1)) <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (S (2 * n + 1))) <> 0
n:nat
INR (S (2 * n + 1)) * INR (fact (2 * n + 1)) <> 0
n:nat
S (S (2 * n + 1)) = (2 * (n + 1) + 1)%nat
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  ring.n:nat
INR 2 <> 0
n:nat
INR (n + 1) <> 0
n:nat
INR (S (2 * (n + 1))) <> 0
n:nat
INR 2 * INR (n + 1) <> 0
n:nat
INR 2 <> 0
n:nat
INR (n + 1) <> 0
n:nat
(2 * (n + 1))%nat = S (2 * n + 1)
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (2 * n + 1)) <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (S (2 * n + 1))) <> 0
n:nat
INR (S (2 * n + 1)) * INR (fact (2 * n + 1)) <> 0
n:nat
S (S (2 * n + 1)) = (2 * (n + 1) + 1)%nat
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  apply not_O_INR; discriminate.n:nat
INR (n + 1) <> 0
n:nat
INR (S (2 * (n + 1))) <> 0
n:nat
INR 2 * INR (n + 1) <> 0
n:nat
INR 2 <> 0
n:nat
INR (n + 1) <> 0
n:nat
(2 * (n + 1))%nat = S (2 * n + 1)
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (2 * n + 1)) <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (S (2 * n + 1))) <> 0
n:nat
INR (S (2 * n + 1)) * INR (fact (2 * n + 1)) <> 0
n:nat
S (S (2 * n + 1)) = (2 * (n + 1) + 1)%nat
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  replace (n + 1)%nat with (S n); [ apply not_O_INR; discriminate | ring ].n:nat
INR (S (2 * (n + 1))) <> 0
n:nat
INR 2 * INR (n + 1) <> 0
n:nat
INR 2 <> 0
n:nat
INR (n + 1) <> 0
n:nat
(2 * (n + 1))%nat = S (2 * n + 1)
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (2 * n + 1)) <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (S (2 * n + 1))) <> 0
n:nat
INR (S (2 * n + 1)) * INR (fact (2 * n + 1)) <> 0
n:nat
S (S (2 * n + 1)) = (2 * (n + 1) + 1)%nat
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  apply not_O_INR; discriminate.n:nat
INR 2 * INR (n + 1) <> 0
n:nat
INR 2 <> 0
n:nat
INR (n + 1) <> 0
n:nat
(2 * (n + 1))%nat = S (2 * n + 1)
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (2 * n + 1)) <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (S (2 * n + 1))) <> 0
n:nat
INR (S (2 * n + 1)) * INR (fact (2 * n + 1)) <> 0
n:nat
S (S (2 * n + 1)) = (2 * (n + 1) + 1)%nat
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  apply prod_neq_R0.n:nat
INR 2 <> 0
n:nat
INR (n + 1) <> 0
n:nat
INR 2 <> 0
n:nat
INR (n + 1) <> 0
n:nat
(2 * (n + 1))%nat = S (2 * n + 1)
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (2 * n + 1)) <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (S (2 * n + 1))) <> 0
n:nat
INR (S (2 * n + 1)) * INR (fact (2 * n + 1)) <> 0
n:nat
S (S (2 * n + 1)) = (2 * (n + 1) + 1)%nat
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  apply not_O_INR; discriminate.n:nat
INR (n + 1) <> 0
n:nat
INR 2 <> 0
n:nat
INR (n + 1) <> 0
n:nat
(2 * (n + 1))%nat = S (2 * n + 1)
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (2 * n + 1)) <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (S (2 * n + 1))) <> 0
n:nat
INR (S (2 * n + 1)) * INR (fact (2 * n + 1)) <> 0
n:nat
S (S (2 * n + 1)) = (2 * (n + 1) + 1)%nat
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  replace (n + 1)%nat with (S n); [ apply not_O_INR; discriminate | ring ].n:nat
INR 2 <> 0
n:nat
INR (n + 1) <> 0
n:nat
(2 * (n + 1))%nat = S (2 * n + 1)
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (2 * n + 1)) <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (S (2 * n + 1))) <> 0
n:nat
INR (S (2 * n + 1)) * INR (fact (2 * n + 1)) <> 0
n:nat
S (S (2 * n + 1)) = (2 * (n + 1) + 1)%nat
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  apply not_O_INR; discriminate.n:nat
INR (n + 1) <> 0
n:nat
(2 * (n + 1))%nat = S (2 * n + 1)
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (2 * n + 1)) <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (S (2 * n + 1))) <> 0
n:nat
INR (S (2 * n + 1)) * INR (fact (2 * n + 1)) <> 0
n:nat
S (S (2 * n + 1)) = (2 * (n + 1) + 1)%nat
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  replace (n + 1)%nat with (S n); [ apply not_O_INR; discriminate | ring ].n:nat
(2 * (n + 1))%nat = S (2 * n + 1)
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (2 * n + 1)) <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (S (2 * n + 1))) <> 0
n:nat
INR (S (2 * n + 1)) * INR (fact (2 * n + 1)) <> 0
n:nat
S (S (2 * n + 1)) = (2 * (n + 1) + 1)%nat
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  rewrite mult_plus_distr_l; cut (forall n:nat, S n = (n + 1)%nat).n:nat
(forall n0 : nat, S n0 = (n0 + 1)%nat) ->
(2 * n + 2 * 1)%nat = S (2 * n + 1)
n:nat
forall n0 : nat, S n0 = (n0 + 1)%nat
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (2 * n + 1)) <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (S (2 * n + 1))) <> 0
n:nat
INR (S (2 * n + 1)) * INR (fact (2 * n + 1)) <> 0
n:nat
S (S (2 * n + 1)) = (2 * (n + 1) + 1)%nat
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  intros; rewrite (H (2 * n + 1)%nat).n:nat
H:forall n0 : nat, S n0 = (n0 + 1)%nat
(2 * n + 2 * 1)%nat = (2 * n + 1 + 1)%nat
n:nat
forall n0 : nat, S n0 = (n0 + 1)%nat
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (2 * n + 1)) <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (S (2 * n + 1))) <> 0
n:nat
INR (S (2 * n + 1)) * INR (fact (2 * n + 1)) <> 0
n:nat
S (S (2 * n + 1)) = (2 * (n + 1) + 1)%nat
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  ring.n:nat
forall n0 : nat, S n0 = (n0 + 1)%nat
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (2 * n + 1)) <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (S (2 * n + 1))) <> 0
n:nat
INR (S (2 * n + 1)) * INR (fact (2 * n + 1)) <> 0
n:nat
S (S (2 * n + 1)) = (2 * (n + 1) + 1)%nat
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  intros; ring.n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (2 * n + 1)) <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (S (2 * n + 1))) <> 0
n:nat
INR (S (2 * n + 1)) * INR (fact (2 * n + 1)) <> 0
n:nat
S (S (2 * n + 1)) = (2 * (n + 1) + 1)%nat
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  apply INR_fact_neq_0.n:nat
INR (S (2 * n + 1)) <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (S (2 * n + 1))) <> 0
n:nat
INR (S (2 * n + 1)) * INR (fact (2 * n + 1)) <> 0
n:nat
S (S (2 * n + 1)) = (2 * (n + 1) + 1)%nat
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  apply not_O_INR; discriminate.n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
INR (S (S (2 * n + 1))) <> 0
n:nat
INR (S (2 * n + 1)) * INR (fact (2 * n + 1)) <> 0
n:nat
S (S (2 * n + 1)) = (2 * (n + 1) + 1)%nat
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  apply INR_fact_neq_0.n:nat
INR (S (S (2 * n + 1))) <> 0
n:nat
INR (S (2 * n + 1)) * INR (fact (2 * n + 1)) <> 0
n:nat
S (S (2 * n + 1)) = (2 * (n + 1) + 1)%nat
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  apply not_O_INR; discriminate.n:nat
INR (S (2 * n + 1)) * INR (fact (2 * n + 1)) <> 0
n:nat
S (S (2 * n + 1)) = (2 * (n + 1) + 1)%nat
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  apply prod_neq_R0; [ apply not_O_INR; discriminate | apply INR_fact_neq_0 ].n:nat
S (S (2 * n + 1)) = (2 * (n + 1) + 1)%nat
n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  cut (forall n:nat, S (S n) = (n + 2)%nat);
    [ intros; rewrite (H (2 * n + 1)%nat); ring | intros; ring ].n:nat
(-1) ^ n <> 0
n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  apply pow_nonzero; discrR.n:nat
INR (fact (2 * n + 1)) <> 0
n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  apply INR_fact_neq_0.n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  apply pow_nonzero; discrR.n:nat
/ INR (fact (2 * n + 1)) <> 0
  apply Rinv_neq_0_compat; apply INR_fact_neq_0.
Qed.

Lemma Alembert_sin : Un_cv (fun n:nat => Rabs (sin_n (S n) / sin_n n)) 0.Un_cv (fun n : nat => Rabs (sin_n (S n) / sin_n n)) 0
Proof.Un_cv (fun n : nat => Rabs (sin_n (S n) / sin_n n)) 0
  unfold Un_cv; intros; assert (H0 := archimed_cor1 eps H).eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
exists N : nat,
  forall n : nat,
  (n >= N)%nat ->
  R_dist (Rabs (sin_n (S n) / sin_n n)) 0 < eps
  elim H0; intros; exists x.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
forall n : nat,
(n >= x)%nat ->
R_dist (Rabs (sin_n (S n) / sin_n n)) 0 < eps
  intros; rewrite simpl_sin_n; unfold R_dist; unfold Rminus;
    rewrite Ropp_0; rewrite Rplus_0_r; rewrite Rabs_Rabsolu;
      rewrite Rabs_Ropp; rewrite Rabs_right.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  rewrite mult_INR; rewrite Rinv_mult_distr.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n + 1) * / INR (2 * S n) < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  cut (/ INR (2 * S n) < 1).eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1 ->
/ INR (2 * S n + 1) * / INR (2 * S n) < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  intro; cut (/ INR (2 * S n + 1) < eps).eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
/ INR (2 * S n + 1) < eps ->
/ INR (2 * S n + 1) * / INR (2 * S n) < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
/ INR (2 * S n + 1) < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  intro; rewrite <- (Rmult_1_l eps); rewrite (Rmult_comm (/ INR (2 * S n + 1)));
    apply Rmult_gt_0_lt_compat; try assumption.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:/ INR (2 * S n + 1) < eps
/ INR (2 * S n + 1) > 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:/ INR (2 * S n + 1) < eps
1 > 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
/ INR (2 * S n + 1) < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  change (0 < / INR (2 * S n + 1)); apply Rinv_0_lt_compat;
    apply lt_INR_0; replace (2 * S n + 1)%nat with (S (2 * S n));
      [ apply lt_O_Sn | ring ].eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:/ INR (2 * S n + 1) < eps
1 > 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
/ INR (2 * S n + 1) < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  apply Rlt_0_1.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
/ INR (2 * S n + 1) < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  cut (x < 2 * S n + 1)%nat.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(x < 2 * S n + 1)%nat -> / INR (2 * S n + 1) < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(x < 2 * S n + 1)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  intro; assert (H5 := lt_INR _ _ H4); apply Rlt_trans with (/ INR x).eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * S n + 1)%nat
H5:INR x < INR (2 * S n + 1)
/ INR (2 * S n + 1) < / INR x
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * S n + 1)%nat
H5:INR x < INR (2 * S n + 1)
/ INR x < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(x < 2 * S n + 1)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  apply Rinv_lt_contravar.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * S n + 1)%nat
H5:INR x < INR (2 * S n + 1)
0 < INR x * INR (2 * S n + 1)
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * S n + 1)%nat
H5:INR x < INR (2 * S n + 1)
INR x < INR (2 * S n + 1)
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * S n + 1)%nat
H5:INR x < INR (2 * S n + 1)
/ INR x < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(x < 2 * S n + 1)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  apply Rmult_lt_0_compat.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * S n + 1)%nat
H5:INR x < INR (2 * S n + 1)
0 < INR x
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * S n + 1)%nat
H5:INR x < INR (2 * S n + 1)
0 < INR (2 * S n + 1)
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * S n + 1)%nat
H5:INR x < INR (2 * S n + 1)
INR x < INR (2 * S n + 1)
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * S n + 1)%nat
H5:INR x < INR (2 * S n + 1)
/ INR x < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(x < 2 * S n + 1)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  apply lt_INR_0; elim H1; intros; assumption.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * S n + 1)%nat
H5:INR x < INR (2 * S n + 1)
0 < INR (2 * S n + 1)
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * S n + 1)%nat
H5:INR x < INR (2 * S n + 1)
INR x < INR (2 * S n + 1)
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * S n + 1)%nat
H5:INR x < INR (2 * S n + 1)
/ INR x < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(x < 2 * S n + 1)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  apply lt_INR_0; replace (2 * S n + 1)%nat with (S (2 * S n));
    [ apply lt_O_Sn | ring ].eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * S n + 1)%nat
H5:INR x < INR (2 * S n + 1)
INR x < INR (2 * S n + 1)
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * S n + 1)%nat
H5:INR x < INR (2 * S n + 1)
/ INR x < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(x < 2 * S n + 1)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  assumption.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
H4:(x < 2 * S n + 1)%nat
H5:INR x < INR (2 * S n + 1)
/ INR x < eps
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(x < 2 * S n + 1)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  elim H1; intros; assumption.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(x < 2 * S n + 1)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  apply lt_le_trans with (S n).eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(x < S n)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(S n <= 2 * S n + 1)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  unfold ge in H2; apply le_lt_n_Sm; assumption.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(S n <= 2 * S n + 1)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  replace (2 * S n + 1)%nat with (S (2 * S n)) by ring.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
H3:/ INR (2 * S n) < 1
(S n <= S (2 * S n))%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  apply le_S; apply le_n_2n.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR (2 * S n) < 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  apply Rmult_lt_reg_l with (INR (2 * S n)).eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
0 < INR (2 * S n)
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) * / INR (2 * S n) < INR (2 * S n) * 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  apply lt_INR_0; replace (2 * S n)%nat with (S (S (2 * n)));
    [ apply lt_O_Sn | ring ].eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) * / INR (2 * S n) < INR (2 * S n) * 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  rewrite <- Rinv_r_sym.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
1 < INR (2 * S n) * 1
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  rewrite Rmult_1_r.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
1 < INR (2 * S n)
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  apply (lt_INR 1).eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
(1 < 2 * S n)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  replace (2 * S n)%nat with (S (S (2 * n))).eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
(1 < S (S (2 * n)))%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
S (S (2 * n)) = (2 * S n)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  apply lt_n_S; apply lt_O_Sn.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
S (S (2 * n)) = (2 * S n)%nat
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  ring.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  apply not_O_INR; discriminate.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n + 1) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  apply not_O_INR; discriminate.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
INR (2 * S n) <> 0
eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  apply not_O_INR; discriminate.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
/ INR ((2 * S n + 1) * (2 * S n)) >= 0
  left; apply Rinv_0_lt_compat.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
0 < INR ((2 * S n + 1) * (2 * S n))
  apply lt_INR_0.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
(0 < (2 * S n + 1) * (2 * S n))%nat
  replace ((2 * S n + 1) * (2 * S n))%nat with
  (6 + (4 * (n * n) + 10 * n))%nat by ring.eps:R
H:eps > 0
H0:exists N : nat, / INR N < eps /\ (0 < N)%nat
x:nat
H1:/ INR x < eps /\ (0 < x)%nat
n:nat
H2:(n >= x)%nat
(0 < 6 + (4 * (n * n) + 10 * n))%nat
  apply lt_O_Sn.
Qed.

Lemma sin_no_R0 : forall n:nat, sin_n n <> 0.forall n : nat, sin_n n <> 0
Proof.forall n : nat, sin_n n <> 0
  intro; unfold sin_n; unfold Rdiv; apply prod_neq_R0.n:nat
(-1) ^ n <> 0
n:nat
/ INR (fact (2 * n + 1)) <> 0
  apply pow_nonzero; discrR.n:nat
/ INR (fact (2 * n + 1)) <> 0
  apply Rinv_neq_0_compat; apply INR_fact_neq_0.
Qed.

(**********)
Definition sin_in (x l:R) : Prop :=
  infinite_sum (fun i:nat => sin_n i * x ^ i) l.

(**********)
Lemma exist_sin : forall x:R, { l:R | sin_in x l }.forall x : R, {l : R | sin_in x l}
Proof.forall x : R, {l : R | sin_in x l}
  intro; generalize (Alembert_C3 sin_n x sin_no_R0 Alembert_sin).x:R
{l : R | Pser sin_n x l} -> {l : R | sin_in x l}
  unfold Pser, sin_n; trivial.
Defined.

(***********************)
(* Definition of sinus *)
Definition sin (x:R) : R := let (a,_) := exist_sin (Rsqr x) in x * a.

(*********************************************)

Properties

(*********************************************)

Lemma cos_sym : forall x:R, cos x = cos (- x).forall x : R, cos x = cos (- x)
Proof.forall x : R, cos x = cos (- x)
  intros; unfold cos; replace (Rsqr (- x)) with (Rsqr x).x:R
(let (a, _) := exist_cos x² in a) =
(let (a, _) := exist_cos x² in a)
x:R
x² = (- x)²
  reflexivity.x:R
x² = (- x)²
  apply Rsqr_neg.
Qed.

Lemma sin_antisym : forall x:R, sin (- x) = - sin x.forall x : R, sin (- x) = - sin x
Proof.forall x : R, sin (- x) = - sin x
  intro; unfold sin; replace (Rsqr (- x)) with (Rsqr x);
    [ idtac | apply Rsqr_neg ].x:R
(let (a, _) := exist_sin x² in - x * a) =
- (let (a, _) := exist_sin x² in x * a)
  case (exist_sin (Rsqr x)); intros; ring.
Qed.

Lemma sin_0 : sin 0 = 0.sin 0 = 0
Proof.sin 0 = 0
  unfold sin; case (exist_sin (Rsqr 0)).forall x : R, sin_in 0² x -> 0 * x = 0
  intros; ring.
Qed.

Lemma exist_cos0 : { l:R | cos_in 0 l }.{l : R | cos_in 0 l}
Proof.{l : R | cos_in 0 l}
  exists 1.cos_in 0 1
  unfold cos_in; unfold infinite_sum; intros; exists 0%nat.eps:R
H:eps > 0
forall n : nat,
(n >= 0)%nat ->
R_dist (sum_f_R0 (fun i : nat => cos_n i * 0 ^ i) n) 1 <
eps
  intros.eps:R
H:eps > 0
n:nat
H0:(n >= 0)%nat
R_dist (sum_f_R0 (fun i : nat => cos_n i * 0 ^ i) n) 1 <
eps
  unfold R_dist.eps:R
H:eps > 0
n:nat
H0:(n >= 0)%nat
Rabs (sum_f_R0 (fun i : nat => cos_n i * 0 ^ i) n - 1) <
eps
  induction  n as [| n Hrecn].eps:R
H:eps > 0
H0:(0 >= 0)%nat
Rabs (sum_f_R0 (fun i : nat => cos_n i * 0 ^ i) 0 - 1) <
eps
eps:R
H:eps > 0
n:nat
H0:(S n >= 0)%nat
Hrecn:(n >= 0)%nat ->
Rabs
  (sum_f_R0 (fun i : nat => cos_n i * 0 ^ i) n -
   1) < eps
Rabs
  (sum_f_R0 (fun i : nat => cos_n i * 0 ^ i) (S n) - 1) <
eps
  unfold cos_n; simpl.eps:R
H:eps > 0
H0:(0 >= 0)%nat
Rabs (1 / 1 * 1 - 1) < eps
eps:R
H:eps > 0
n:nat
H0:(S n >= 0)%nat
Hrecn:(n >= 0)%nat ->
Rabs
  (sum_f_R0 (fun i : nat => cos_n i * 0 ^ i) n -
   1) < eps
Rabs
  (sum_f_R0 (fun i : nat => cos_n i * 0 ^ i) (S n) - 1) <
eps
  unfold Rdiv; rewrite Rinv_1.eps:R
H:eps > 0
H0:(0 >= 0)%nat
Rabs (1 * 1 * 1 - 1) < eps
eps:R
H:eps > 0
n:nat
H0:(S n >= 0)%nat
Hrecn:(n >= 0)%nat ->
Rabs
  (sum_f_R0 (fun i : nat => cos_n i * 0 ^ i) n -
   1) < eps
Rabs
  (sum_f_R0 (fun i : nat => cos_n i * 0 ^ i) (S n) - 1) <
eps
  do 2 rewrite Rmult_1_r.eps:R
H:eps > 0
H0:(0 >= 0)%nat
Rabs (1 - 1) < eps
eps:R
H:eps > 0
n:nat
H0:(S n >= 0)%nat
Hrecn:(n >= 0)%nat ->
Rabs
  (sum_f_R0 (fun i : nat => cos_n i * 0 ^ i) n -
   1) < eps
Rabs
  (sum_f_R0 (fun i : nat => cos_n i * 0 ^ i) (S n) - 1) <
eps
  unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption.eps:R
H:eps > 0
n:nat
H0:(S n >= 0)%nat
Hrecn:(n >= 0)%nat ->
Rabs
  (sum_f_R0 (fun i : nat => cos_n i * 0 ^ i) n -
   1) < eps
Rabs
  (sum_f_R0 (fun i : nat => cos_n i * 0 ^ i) (S n) - 1) <
eps
  rewrite tech5.eps:R
H:eps > 0
n:nat
H0:(S n >= 0)%nat
Hrecn:(n >= 0)%nat ->
Rabs
  (sum_f_R0 (fun i : nat => cos_n i * 0 ^ i) n -
   1) < eps
Rabs
  (sum_f_R0 (fun i : nat => cos_n i * 0 ^ i) n +
   cos_n (S n) * 0 ^ S n - 1) < eps
  replace (cos_n (S n) * 0 ^ S n) with 0.eps:R
H:eps > 0
n:nat
H0:(S n >= 0)%nat
Hrecn:(n >= 0)%nat ->
Rabs
  (sum_f_R0 (fun i : nat => cos_n i * 0 ^ i) n -
   1) < eps
Rabs
  (sum_f_R0 (fun i : nat => cos_n i * 0 ^ i) n + 0 - 1) <
eps
eps:R
H:eps > 0
n:nat
H0:(S n >= 0)%nat
Hrecn:(n >= 0)%nat ->
Rabs
  (sum_f_R0 (fun i : nat => cos_n i * 0 ^ i) n -
   1) < eps
0 = cos_n (S n) * 0 ^ S n
  rewrite Rplus_0_r.eps:R
H:eps > 0
n:nat
H0:(S n >= 0)%nat
Hrecn:(n >= 0)%nat ->
Rabs
  (sum_f_R0 (fun i : nat => cos_n i * 0 ^ i) n -
   1) < eps
Rabs (sum_f_R0 (fun i : nat => cos_n i * 0 ^ i) n - 1) <
eps
eps:R
H:eps > 0
n:nat
H0:(S n >= 0)%nat
Hrecn:(n >= 0)%nat ->
Rabs
  (sum_f_R0 (fun i : nat => cos_n i * 0 ^ i) n -
   1) < eps
0 = cos_n (S n) * 0 ^ S n
  apply Hrecn; unfold ge; apply le_O_n.eps:R
H:eps > 0
n:nat
H0:(S n >= 0)%nat
Hrecn:(n >= 0)%nat ->
Rabs
  (sum_f_R0 (fun i : nat => cos_n i * 0 ^ i) n -
   1) < eps
0 = cos_n (S n) * 0 ^ S n
  simpl; ring.
Defined.

(* Value of [cos 0] *)
Lemma cos_0 : cos 0 = 1.cos 0 = 1
Proof.cos 0 = 1
  cut (cos_in 0 (cos 0)).cos_in 0 (cos 0) -> cos 0 = 1
cos_in 0 (cos 0)
  cut (cos_in 0 1).cos_in 0 1 -> cos_in 0 (cos 0) -> cos 0 = 1
cos_in 0 1
cos_in 0 (cos 0)
  unfold cos_in; intros; eapply uniqueness_sum.H:infinite_sum (fun i : nat => cos_n i * 0 ^ i) 1
H0:infinite_sum (fun i : nat => cos_n i * 0 ^ i)
  (cos 0)
infinite_sum ?An (cos 0)
H:infinite_sum (fun i : nat => cos_n i * 0 ^ i) 1
H0:infinite_sum (fun i : nat => cos_n i * 0 ^ i)
  (cos 0)
infinite_sum ?An 1
cos_in 0 1
cos_in 0 (cos 0)
  apply H0.H:infinite_sum (fun i : nat => cos_n i * 0 ^ i) 1
H0:infinite_sum (fun i : nat => cos_n i * 0 ^ i)
  (cos 0)
infinite_sum (fun i : nat => cos_n i * 0 ^ i) 1
cos_in 0 1
cos_in 0 (cos 0)
  apply H.cos_in 0 1
cos_in 0 (cos 0)
  exact (proj2_sig exist_cos0).cos_in 0 (cos 0)
  assert (H := proj2_sig (exist_cos (Rsqr 0))); unfold cos;
    pattern 0 at 1; replace 0 with (Rsqr 0); [ exact H | apply Rsqr_0 ].
Qed.