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)         *)
(************************************************************************)

(*i Some properties about pow and sum have been made with John Harrison i*)
(*i Some Lemmas (about pow and powerRZ) have been done by Laurent Thery i*)

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

Definition of the sum functions

(*                                                      *)
(********************************************************)
Require Export ArithRing.

Require Import Rbase.
Require Export Rpow_def.
Require Export R_Ifp.
Require Export Rbasic_fun.
Require Export R_sqr.
Require Export SplitAbsolu.
Require Export SplitRmult.
Require Export ArithProp.
Require Import Omega.
Require Import Zpower.
Local Open Scope nat_scope.
Local Open Scope R_scope.

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

Lemmas about factorial

(*******************************)
(*********)
Lemma INR_fact_neq_0 : forall n:nat, INR (fact n) <> 0.forall n : nat, INR (fact n) <> 0
Proof.forall n : nat, INR (fact n) <> 0
  intro; red; intro; apply (not_O_INR (fact n) (fact_neq_0 n));
    assumption.
Qed.

(*********)
Lemma fact_simpl : forall n:nat, fact (S n) = (S n * fact n)%nat.forall n : nat, fact (S n) = (S n * fact n)%nat
Proof.forall n : nat, fact (S n) = (S n * fact n)%nat
  intro; reflexivity.
Qed.

(*********)
Lemma simpl_fact :
  forall n:nat, / INR (fact (S n)) * / / INR (fact n) = / INR (S n).forall n : nat,
/ INR (fact (S n)) * / / INR (fact n) = / INR (S n)
Proof.forall n : nat,
/ INR (fact (S n)) * / / INR (fact n) = / INR (S n)
  intro; rewrite (Rinv_involutive (INR (fact n)) (INR_fact_neq_0 n));
    unfold fact at 1; cbv beta iota; fold fact;
      rewrite (mult_INR (S n) (fact n));
        rewrite (Rinv_mult_distr (INR (S n)) (INR (fact n))).n:nat
/ INR (S n) * / INR (fact n) * INR (fact n) =
/ INR (S n)
n:nat
INR (S n) <> 0
n:nat
INR (fact n) <> 0
  rewrite (Rmult_assoc (/ INR (S n)) (/ INR (fact n)) (INR (fact n)));
    rewrite (Rinv_l (INR (fact n)) (INR_fact_neq_0 n));
      apply (let (H1, H2) := Rmult_ne (/ INR (S n)) in H1).n:nat
INR (S n) <> 0
n:nat
INR (fact n) <> 0
  apply not_O_INR; auto.n:nat
INR (fact n) <> 0
  apply INR_fact_neq_0.
Qed.

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

Power

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

Infix "^" := pow : R_scope.

Lemma pow_O : forall x:R, x ^ 0 = 1.forall x : R, x ^ 0 = 1
Proof.forall x : R, x ^ 0 = 1
  reflexivity.
Qed.

Lemma pow_1 : forall x:R, x ^ 1 = x.forall x : R, x ^ 1 = x
Proof.forall x : R, x ^ 1 = x
  simpl; auto with real.
Qed.

Lemma pow_add : forall (x:R) (n m:nat), x ^ (n + m) = x ^ n * x ^ m.forall (x : R) (n m : nat),
x ^ (n + m) = x ^ n * x ^ m
Proof.forall (x : R) (n m : nat),
x ^ (n + m) = x ^ n * x ^ m
  intros x n; elim n; simpl; auto with real.x:R
n:nat
forall n0 : nat,
(forall m : nat, x ^ (n0 + m) = x ^ n0 * x ^ m) ->
forall m : nat, x * x ^ (n0 + m) = x * x ^ n0 * x ^ m
  intros n0 H' m; rewrite H'; auto with real.
Qed.

Lemma Rpow_mult_distr : forall (x y:R) (n:nat), (x * y) ^ n = x^n * y^n.forall (x y : R) (n : nat),
(x * y) ^ n = x ^ n * y ^ n
Proof.forall (x y : R) (n : nat),
(x * y) ^ n = x ^ n * y ^ n
intros x y n ; induction n.x, y:R
(x * y) ^ 0 = x ^ 0 * y ^ 0
x, y:R
n:nat
IHn:(x * y) ^ n = x ^ n * y ^ n
(x * y) ^ S n = x ^ S n * y ^ S n
 field.x, y:R
n:nat
IHn:(x * y) ^ n = x ^ n * y ^ n
(x * y) ^ S n = x ^ S n * y ^ S n
 simpl.x, y:R
n:nat
IHn:(x * y) ^ n = x ^ n * y ^ n
x * y * (x * y) ^ n = x * x ^ n * (y * y ^ n)
 repeat (rewrite Rmult_assoc) ; apply Rmult_eq_compat_l.x, y:R
n:nat
IHn:(x * y) ^ n = x ^ n * y ^ n
y * (x * y) ^ n = x ^ n * (y * y ^ n)
 rewrite IHn ; field.
Qed.

Lemma pow_nonzero : forall (x:R) (n:nat), x <> 0 -> x ^ n <> 0.forall (x : R) (n : nat), x <> 0 -> x ^ n <> 0
Proof.forall (x : R) (n : nat), x <> 0 -> x ^ n <> 0
  intro; simple induction n; simpl.x:R
n:nat
x <> 0 -> 1 <> 0
x:R
n:nat
forall n0 : nat,
(x <> 0 -> x ^ n0 <> 0) -> x <> 0 -> x * x ^ n0 <> 0
  intro; red; intro; apply R1_neq_R0; assumption.x:R
n:nat
forall n0 : nat,
(x <> 0 -> x ^ n0 <> 0) -> x <> 0 -> x * x ^ n0 <> 0
  intros; red; intro; elim (Rmult_integral x (x ^ n0) H1).x:R
n, n0:nat
H:x <> 0 -> x ^ n0 <> 0
H0:x <> 0
H1:x * x ^ n0 = 0
x = 0 -> False
x:R
n, n0:nat
H:x <> 0 -> x ^ n0 <> 0
H0:x <> 0
H1:x * x ^ n0 = 0
x ^ n0 = 0 -> False
  intro; auto.x:R
n, n0:nat
H:x <> 0 -> x ^ n0 <> 0
H0:x <> 0
H1:x * x ^ n0 = 0
x ^ n0 = 0 -> False
  apply H; assumption.
Qed.

Hint Resolve pow_O pow_1 pow_add pow_nonzero: real.

Lemma pow_RN_plus :
  forall (x:R) (n m:nat), x <> 0 -> x ^ n = x ^ (n + m) * / x ^ m.forall (x : R) (n m : nat),
x <> 0 -> x ^ n = x ^ (n + m) * / x ^ m
Proof.forall (x : R) (n m : nat),
x <> 0 -> x ^ n = x ^ (n + m) * / x ^ m
  intros x n; elim n; simpl; auto with real.x:R
n:nat
forall n0 : nat,
(forall m : nat,
 x <> 0 -> x ^ n0 = x ^ (n0 + m) * / x ^ m) ->
forall m : nat,
x <> 0 -> x * x ^ n0 = x * x ^ (n0 + m) * / x ^ m
  intros n0 H' m H'0.x:R
n, n0:nat
H':forall m0 : nat,
x <> 0 -> x ^ n0 = x ^ (n0 + m0) * / x ^ m0
m:nat
H'0:x <> 0
x * x ^ n0 = x * x ^ (n0 + m) * / x ^ m
  rewrite Rmult_assoc; rewrite <- H'; auto.
Qed.

Lemma pow_lt : forall (x:R) (n:nat), 0 < x -> 0 < x ^ n.forall (x : R) (n : nat), 0 < x -> 0 < x ^ n
Proof.forall (x : R) (n : nat), 0 < x -> 0 < x ^ n
  intros x n; elim n; simpl; auto with real.x:R
n:nat
forall n0 : nat,
(0 < x -> 0 < x ^ n0) -> 0 < x -> 0 < x * x ^ n0
  intros n0 H' H'0; replace 0 with (x * 0); auto with real.
Qed.
Hint Resolve pow_lt: real.

Lemma Rlt_pow_R1 : forall (x:R) (n:nat), 1 < x -> (0 < n)%nat -> 1 < x ^ n.forall (x : R) (n : nat),
1 < x -> (0 < n)%nat -> 1 < x ^ n
Proof.forall (x : R) (n : nat),
1 < x -> (0 < n)%nat -> 1 < x ^ n
  intros x n; elim n; simpl; auto with real.x:R
n:nat
1 < x -> (0 < 0)%nat -> 1 < 1
x:R
n:nat
forall n0 : nat,
(1 < x -> (0 < n0)%nat -> 1 < x ^ n0) ->
1 < x -> (0 < S n0)%nat -> 1 < x * x ^ n0
  intros H' H'0; exfalso; omega.x:R
n:nat
forall n0 : nat,
(1 < x -> (0 < n0)%nat -> 1 < x ^ n0) ->
1 < x -> (0 < S n0)%nat -> 1 < x * x ^ n0
  intros n0; case n0.x:R
n, n0:nat
(1 < x -> (0 < 0)%nat -> 1 < x ^ 0) ->
1 < x -> (0 < 1)%nat -> 1 < x * x ^ 0
x:R
n, n0:nat
forall n1 : nat,
(1 < x -> (0 < S n1)%nat -> 1 < x ^ S n1) ->
1 < x -> (0 < S (S n1))%nat -> 1 < x * x ^ S n1
  simpl; rewrite Rmult_1_r; auto.x:R
n, n0:nat
forall n1 : nat,
(1 < x -> (0 < S n1)%nat -> 1 < x ^ S n1) ->
1 < x -> (0 < S (S n1))%nat -> 1 < x * x ^ S n1
  intros n1 H' H'0 H'1.x:R
n, n0, n1:nat
H':1 < x -> (0 < S n1)%nat -> 1 < x ^ S n1
H'0:1 < x
H'1:(0 < S (S n1))%nat
1 < x * x ^ S n1
  replace 1 with (1 * 1); auto with real.x:R
n, n0, n1:nat
H':1 < x -> (0 < S n1)%nat -> 1 < x ^ S n1
H'0:1 < x
H'1:(0 < S (S n1))%nat
1 * 1 < x * x ^ S n1
  apply Rlt_trans with (r2 := x * 1); auto with real.x:R
n, n0, n1:nat
H':1 < x -> (0 < S n1)%nat -> 1 < x ^ S n1
H'0:1 < x
H'1:(0 < S (S n1))%nat
x * 1 < x * x ^ S n1
  apply Rmult_lt_compat_l; auto with real.x:R
n, n0, n1:nat
H':1 < x -> (0 < S n1)%nat -> 1 < x ^ S n1
H'0:1 < x
H'1:(0 < S (S n1))%nat
0 < x
x:R
n, n0, n1:nat
H':1 < x -> (0 < S n1)%nat -> 1 < x ^ S n1
H'0:1 < x
H'1:(0 < S (S n1))%nat
1 < x ^ S n1
  apply Rlt_trans with (r2 := 1); auto with real.x:R
n, n0, n1:nat
H':1 < x -> (0 < S n1)%nat -> 1 < x ^ S n1
H'0:1 < x
H'1:(0 < S (S n1))%nat
1 < x ^ S n1
  apply H'; auto with arith.
Qed.
Hint Resolve Rlt_pow_R1: real.

Lemma Rlt_pow : forall (x:R) (n m:nat), 1 < x -> (n < m)%nat -> x ^ n < x ^ m.forall (x : R) (n m : nat),
1 < x -> (n < m)%nat -> x ^ n < x ^ m
Proof.forall (x : R) (n m : nat),
1 < x -> (n < m)%nat -> x ^ n < x ^ m
  intros x n m H' H'0; replace m with (m - n + n)%nat.x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
x ^ n < x ^ (m - n + n)
x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
(m - n + n)%nat = m
  rewrite pow_add.x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
x ^ n < x ^ (m - n) * x ^ n
x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
(m - n + n)%nat = m
  pattern (x ^ n) at 1; replace (x ^ n) with (1 * x ^ n);
    auto with real.x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
1 * x ^ n < x ^ (m - n) * x ^ n
x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
(m - n + n)%nat = m
  apply Rminus_lt.x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
1 * x ^ n - x ^ (m - n) * x ^ n < 0
x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
(m - n + n)%nat = m
  repeat rewrite (fun y:R => Rmult_comm y (x ^ n));
    rewrite <- Rmult_minus_distr_l.x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
x ^ n * (1 - x ^ (m - n)) < 0
x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
(m - n + n)%nat = m
  replace 0 with (x ^ n * 0); auto with real.x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
x ^ n * (1 - x ^ (m - n)) < x ^ n * 0
x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
(m - n + n)%nat = m
  apply Rmult_lt_compat_l; auto with real.x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
0 < x ^ n
x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
1 - x ^ (m - n) < 0
x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
(m - n + n)%nat = m
  apply pow_lt; auto with real.x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
0 < x
x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
1 - x ^ (m - n) < 0
x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
(m - n + n)%nat = m
  apply Rlt_trans with (r2 := 1); auto with real.x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
1 - x ^ (m - n) < 0
x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
(m - n + n)%nat = m
  apply Rlt_minus; auto with real.x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
1 < x ^ (m - n)
x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
(m - n + n)%nat = m
  apply Rlt_pow_R1; auto with arith.x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
(0 < m - n)%nat
x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
(m - n + n)%nat = m
  apply plus_lt_reg_l with (p := n); auto with arith.x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
(n + 0 < n + (m - n))%nat
x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
(m - n + n)%nat = m
  rewrite le_plus_minus_r; auto with arith; rewrite <- plus_n_O; auto.x:R
n, m:nat
H':1 < x
H'0:(n < m)%nat
(m - n + n)%nat = m
  rewrite plus_comm; auto with arith.
Qed.
Hint Resolve Rlt_pow: real.

(*********)
Lemma tech_pow_Rmult : forall (x:R) (n:nat), x * x ^ n = x ^ S n.forall (x : R) (n : nat), x * x ^ n = x ^ S n
Proof.forall (x : R) (n : nat), x * x ^ n = x ^ S n
  simple induction n; simpl; trivial.
Qed.

(*********)
Lemma tech_pow_Rplus :
  forall (x:R) (a n:nat), x ^ a + INR n * x ^ a = INR (S n) * x ^ a.forall (x : R) (a n : nat),
x ^ a + INR n * x ^ a = INR (S n) * x ^ a
Proof.forall (x : R) (a n : nat),
x ^ a + INR n * x ^ a = INR (S n) * x ^ a
  intros; pattern (x ^ a) at 1;
    rewrite <- (let (H1, H2) := Rmult_ne (x ^ a) in H1);
      rewrite (Rmult_comm (INR n) (x ^ a));
        rewrite <- (Rmult_plus_distr_l (x ^ a) 1 (INR n));
          rewrite (Rplus_comm 1 (INR n)); rewrite <- (S_INR n);
            apply Rmult_comm.
Qed.

Lemma poly : forall (n:nat) (x:R), 0 < x -> 1 + INR n * x <= (1 + x) ^ n.forall (n : nat) (x : R),
0 < x -> 1 + INR n * x <= (1 + x) ^ n
Proof.forall (n : nat) (x : R),
0 < x -> 1 + INR n * x <= (1 + x) ^ n
  intros; elim n.n:nat
x:R
H:0 < x
1 + INR 0 * x <= (1 + x) ^ 0
n:nat
x:R
H:0 < x
forall n0 : nat,
1 + INR n0 * x <= (1 + x) ^ n0 ->
1 + INR (S n0) * x <= (1 + x) ^ S n0
  simpl; cut (1 + 0 * x = 1).n:nat
x:R
H:0 < x
1 + 0 * x = 1 -> 1 + 0 * x <= 1
n:nat
x:R
H:0 < x
1 + 0 * x = 1
n:nat
x:R
H:0 < x
forall n0 : nat,
1 + INR n0 * x <= (1 + x) ^ n0 ->
1 + INR (S n0) * x <= (1 + x) ^ S n0
  intro; rewrite H0; unfold Rle; right; reflexivity.n:nat
x:R
H:0 < x
1 + 0 * x = 1
n:nat
x:R
H:0 < x
forall n0 : nat,
1 + INR n0 * x <= (1 + x) ^ n0 ->
1 + INR (S n0) * x <= (1 + x) ^ S n0
  ring.n:nat
x:R
H:0 < x
forall n0 : nat,
1 + INR n0 * x <= (1 + x) ^ n0 ->
1 + INR (S n0) * x <= (1 + x) ^ S n0
  intros; unfold pow; fold pow;
    apply
      (Rle_trans (1 + INR (S n0) * x) ((1 + x) * (1 + INR n0 * x))
        ((1 + x) * (1 + x) ^ n0)).n:nat
x:R
H:0 < x
n0:nat
H0:1 + INR n0 * x <= (1 + x) ^ n0
1 + INR (S n0) * x <= (1 + x) * (1 + INR n0 * x)
n:nat
x:R
H:0 < x
n0:nat
H0:1 + INR n0 * x <= (1 + x) ^ n0
(1 + x) * (1 + INR n0 * x) <= (1 + x) * (1 + x) ^ n0
  cut ((1 + x) * (1 + INR n0 * x) = 1 + INR (S n0) * x + INR n0 * (x * x)).n:nat
x:R
H:0 < x
n0:nat
H0:1 + INR n0 * x <= (1 + x) ^ n0
(1 + x) * (1 + INR n0 * x) =
1 + INR (S n0) * x + INR n0 * (x * x) ->
1 + INR (S n0) * x <= (1 + x) * (1 + INR n0 * x)
n:nat
x:R
H:0 < x
n0:nat
H0:1 + INR n0 * x <= (1 + x) ^ n0
(1 + x) * (1 + INR n0 * x) =
1 + INR (S n0) * x + INR n0 * (x * x)
n:nat
x:R
H:0 < x
n0:nat
H0:1 + INR n0 * x <= (1 + x) ^ n0
(1 + x) * (1 + INR n0 * x) <= (1 + x) * (1 + x) ^ n0
  intro; rewrite H1; pattern (1 + INR (S n0) * x) at 1;
    rewrite <- (let (H1, H2) := Rplus_ne (1 + INR (S n0) * x) in H1);
      apply Rplus_le_compat_l; elim n0; intros.n:nat
x:R
H:0 < x
n0:nat
H0:1 + INR n0 * x <= (1 + x) ^ n0
H1:(1 + x) * (1 + INR n0 * x) =
1 + INR (S n0) * x + INR n0 * (x * x)
0 <= INR 0 * (x * x)
n:nat
x:R
H:0 < x
n0:nat
H0:1 + INR n0 * x <= (1 + x) ^ n0
H1:(1 + x) * (1 + INR n0 * x) =
1 + INR (S n0) * x + INR n0 * (x * x)
n1:nat
H2:0 <= INR n1 * (x * x)
0 <= INR (S n1) * (x * x)
n:nat
x:R
H:0 < x
n0:nat
H0:1 + INR n0 * x <= (1 + x) ^ n0
(1 + x) * (1 + INR n0 * x) =
1 + INR (S n0) * x + INR n0 * (x * x)
n:nat
x:R
H:0 < x
n0:nat
H0:1 + INR n0 * x <= (1 + x) ^ n0
(1 + x) * (1 + INR n0 * x) <= (1 + x) * (1 + x) ^ n0
  simpl; rewrite Rmult_0_l; unfold Rle; right; auto.n:nat
x:R
H:0 < x
n0:nat
H0:1 + INR n0 * x <= (1 + x) ^ n0
H1:(1 + x) * (1 + INR n0 * x) =
1 + INR (S n0) * x + INR n0 * (x * x)
n1:nat
H2:0 <= INR n1 * (x * x)
0 <= INR (S n1) * (x * x)
n:nat
x:R
H:0 < x
n0:nat
H0:1 + INR n0 * x <= (1 + x) ^ n0
(1 + x) * (1 + INR n0 * x) =
1 + INR (S n0) * x + INR n0 * (x * x)
n:nat
x:R
H:0 < x
n0:nat
H0:1 + INR n0 * x <= (1 + x) ^ n0
(1 + x) * (1 + INR n0 * x) <= (1 + x) * (1 + x) ^ n0
  unfold Rle; left; generalize Rmult_gt_0_compat; unfold Rgt;
    intro; fold (Rsqr x);
      apply (H3 (INR (S n1)) (Rsqr x) (lt_INR_0 (S n1) (lt_O_Sn n1)));
        fold (x > 0) in H;
          apply (Rlt_0_sqr x (Rlt_dichotomy_converse x 0 (or_intror (x < 0) H))).n:nat
x:R
H:0 < x
n0:nat
H0:1 + INR n0 * x <= (1 + x) ^ n0
(1 + x) * (1 + INR n0 * x) =
1 + INR (S n0) * x + INR n0 * (x * x)
n:nat
x:R
H:0 < x
n0:nat
H0:1 + INR n0 * x <= (1 + x) ^ n0
(1 + x) * (1 + INR n0 * x) <= (1 + x) * (1 + x) ^ n0
  rewrite (S_INR n0); ring.n:nat
x:R
H:0 < x
n0:nat
H0:1 + INR n0 * x <= (1 + x) ^ n0
(1 + x) * (1 + INR n0 * x) <= (1 + x) * (1 + x) ^ n0
  unfold Rle in H0; elim H0; intro.n:nat
x:R
H:0 < x
n0:nat
H0:1 + INR n0 * x < (1 + x) ^ n0 \/
1 + INR n0 * x = (1 + x) ^ n0
H1:1 + INR n0 * x < (1 + x) ^ n0
(1 + x) * (1 + INR n0 * x) <= (1 + x) * (1 + x) ^ n0
n:nat
x:R
H:0 < x
n0:nat
H0:1 + INR n0 * x < (1 + x) ^ n0 \/
1 + INR n0 * x = (1 + x) ^ n0
H1:1 + INR n0 * x = (1 + x) ^ n0
(1 + x) * (1 + INR n0 * x) <= (1 + x) * (1 + x) ^ n0
  unfold Rle; left; apply Rmult_lt_compat_l.n:nat
x:R
H:0 < x
n0:nat
H0:1 + INR n0 * x < (1 + x) ^ n0 \/
1 + INR n0 * x = (1 + x) ^ n0
H1:1 + INR n0 * x < (1 + x) ^ n0
0 < 1 + x
n:nat
x:R
H:0 < x
n0:nat
H0:1 + INR n0 * x < (1 + x) ^ n0 \/
1 + INR n0 * x = (1 + x) ^ n0
H1:1 + INR n0 * x < (1 + x) ^ n0
1 + INR n0 * x < (1 + x) ^ n0
n:nat
x:R
H:0 < x
n0:nat
H0:1 + INR n0 * x < (1 + x) ^ n0 \/
1 + INR n0 * x = (1 + x) ^ n0
H1:1 + INR n0 * x = (1 + x) ^ n0
(1 + x) * (1 + INR n0 * x) <= (1 + x) * (1 + x) ^ n0
  rewrite Rplus_comm; apply (Rle_lt_0_plus_1 x (Rlt_le 0 x H)).n:nat
x:R
H:0 < x
n0:nat
H0:1 + INR n0 * x < (1 + x) ^ n0 \/
1 + INR n0 * x = (1 + x) ^ n0
H1:1 + INR n0 * x < (1 + x) ^ n0
1 + INR n0 * x < (1 + x) ^ n0
n:nat
x:R
H:0 < x
n0:nat
H0:1 + INR n0 * x < (1 + x) ^ n0 \/
1 + INR n0 * x = (1 + x) ^ n0
H1:1 + INR n0 * x = (1 + x) ^ n0
(1 + x) * (1 + INR n0 * x) <= (1 + x) * (1 + x) ^ n0
  assumption.n:nat
x:R
H:0 < x
n0:nat
H0:1 + INR n0 * x < (1 + x) ^ n0 \/
1 + INR n0 * x = (1 + x) ^ n0
H1:1 + INR n0 * x = (1 + x) ^ n0
(1 + x) * (1 + INR n0 * x) <= (1 + x) * (1 + x) ^ n0
  rewrite H1; unfold Rle; right; trivial.
Qed.

Lemma Power_monotonic :
  forall (x:R) (m n:nat),
    Rabs x > 1 -> (m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n).forall (x : R) (m n : nat),
Rabs x > 1 ->
(m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n)
Proof.forall (x : R) (m n : nat),
Rabs x > 1 ->
(m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n)
  intros x m n H; induction  n as [| n Hrecn]; intros; inversion H0.x:R
m:nat
H:Rabs x > 1
H0:(m <= 0)%nat
H1:m = 0%nat
Rabs (x ^ 0) <= Rabs (x ^ 0)
x:R
m, n:nat
H:Rabs x > 1
Hrecn:(m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n)
H0:(m <= S n)%nat
H1:m = S n
Rabs (x ^ S n) <= Rabs (x ^ S n)
x:R
m, n:nat
H:Rabs x > 1
Hrecn:(m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n)
H0:(m <= S n)%nat
m0:nat
H2:(m <= n)%nat
H1:m0 = n
Rabs (x ^ m) <= Rabs (x ^ S n)
  unfold Rle; right; reflexivity.x:R
m, n:nat
H:Rabs x > 1
Hrecn:(m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n)
H0:(m <= S n)%nat
H1:m = S n
Rabs (x ^ S n) <= Rabs (x ^ S n)
x:R
m, n:nat
H:Rabs x > 1
Hrecn:(m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n)
H0:(m <= S n)%nat
m0:nat
H2:(m <= n)%nat
H1:m0 = n
Rabs (x ^ m) <= Rabs (x ^ S n)
  unfold Rle; right; reflexivity.x:R
m, n:nat
H:Rabs x > 1
Hrecn:(m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n)
H0:(m <= S n)%nat
m0:nat
H2:(m <= n)%nat
H1:m0 = n
Rabs (x ^ m) <= Rabs (x ^ S n)
  apply (Rle_trans (Rabs (x ^ m)) (Rabs (x ^ n)) (Rabs (x ^ S n))).x:R
m, n:nat
H:Rabs x > 1
Hrecn:(m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n)
H0:(m <= S n)%nat
m0:nat
H2:(m <= n)%nat
H1:m0 = n
Rabs (x ^ m) <= Rabs (x ^ n)
x:R
m, n:nat
H:Rabs x > 1
Hrecn:(m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n)
H0:(m <= S n)%nat
m0:nat
H2:(m <= n)%nat
H1:m0 = n
Rabs (x ^ n) <= Rabs (x ^ S n)
  apply Hrecn; assumption.x:R
m, n:nat
H:Rabs x > 1
Hrecn:(m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n)
H0:(m <= S n)%nat
m0:nat
H2:(m <= n)%nat
H1:m0 = n
Rabs (x ^ n) <= Rabs (x ^ S n)
  simpl; rewrite Rabs_mult.x:R
m, n:nat
H:Rabs x > 1
Hrecn:(m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n)
H0:(m <= S n)%nat
m0:nat
H2:(m <= n)%nat
H1:m0 = n
Rabs (x ^ n) <= Rabs x * Rabs (x ^ n)
  pattern (Rabs (x ^ n)) at 1.x:R
m, n:nat
H:Rabs x > 1
Hrecn:(m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n)
H0:(m <= S n)%nat
m0:nat
H2:(m <= n)%nat
H1:m0 = n
(fun r : R => r <= Rabs x * Rabs (x ^ n))
  (Rabs (x ^ n))
  rewrite <- Rmult_1_r.x:R
m, n:nat
H:Rabs x > 1
Hrecn:(m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n)
H0:(m <= S n)%nat
m0:nat
H2:(m <= n)%nat
H1:m0 = n
Rabs (x ^ n) * 1 <= Rabs x * Rabs (x ^ n)
  rewrite (Rmult_comm (Rabs x) (Rabs (x ^ n))).x:R
m, n:nat
H:Rabs x > 1
Hrecn:(m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n)
H0:(m <= S n)%nat
m0:nat
H2:(m <= n)%nat
H1:m0 = n
Rabs (x ^ n) * 1 <= Rabs (x ^ n) * Rabs x
  apply Rmult_le_compat_l.x:R
m, n:nat
H:Rabs x > 1
Hrecn:(m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n)
H0:(m <= S n)%nat
m0:nat
H2:(m <= n)%nat
H1:m0 = n
0 <= Rabs (x ^ n)
x:R
m, n:nat
H:Rabs x > 1
Hrecn:(m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n)
H0:(m <= S n)%nat
m0:nat
H2:(m <= n)%nat
H1:m0 = n
1 <= Rabs x
  apply Rabs_pos.x:R
m, n:nat
H:Rabs x > 1
Hrecn:(m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n)
H0:(m <= S n)%nat
m0:nat
H2:(m <= n)%nat
H1:m0 = n
1 <= Rabs x
  unfold Rgt in H.x:R
m, n:nat
H:1 < Rabs x
Hrecn:(m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n)
H0:(m <= S n)%nat
m0:nat
H2:(m <= n)%nat
H1:m0 = n
1 <= Rabs x
  apply Rlt_le; assumption.
Qed.

Lemma RPow_abs : forall (x:R) (n:nat), Rabs x ^ n = Rabs (x ^ n).forall (x : R) (n : nat), Rabs x ^ n = Rabs (x ^ n)
Proof.forall (x : R) (n : nat), Rabs x ^ n = Rabs (x ^ n)
  intro; simple induction n; simpl.x:R
n:nat
1 = Rabs 1
x:R
n:nat
forall n0 : nat,
Rabs x ^ n0 = Rabs (x ^ n0) ->
Rabs x * Rabs x ^ n0 = Rabs (x * x ^ n0)
  symmetry; apply Rabs_pos_eq; apply Rlt_le; apply Rlt_0_1.x:R
n:nat
forall n0 : nat,
Rabs x ^ n0 = Rabs (x ^ n0) ->
Rabs x * Rabs x ^ n0 = Rabs (x * x ^ n0)
  intros; rewrite H; symmetry; apply Rabs_mult.
Qed.


Lemma Pow_x_infinity :
  forall x:R,
    Rabs x > 1 ->
    forall b:R,
      exists N : nat, (forall n:nat, (n >= N)%nat -> Rabs (x ^ n) >= b).forall x : R,
Rabs x > 1 ->
forall b : R,
exists N : nat,
  forall n : nat, (n >= N)%nat -> Rabs (x ^ n) >= b
Proof.forall x : R,
Rabs x > 1 ->
forall b : R,
exists N : nat,
  forall n : nat, (n >= N)%nat -> Rabs (x ^ n) >= b
  intros; elim (archimed (b * / (Rabs x - 1))); intros; clear H1;
    cut (exists N : nat, INR N >= b * / (Rabs x - 1)).x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
(exists N : nat, INR N >= b * / (Rabs x - 1)) ->
exists N : nat,
  forall n : nat, (n >= N)%nat -> Rabs (x ^ n) >= b
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
exists N : nat, INR N >= b * / (Rabs x - 1)
  intro; elim H1; clear H1; intros; exists x0; intros;
    apply (Rge_trans (Rabs (x ^ n)) (Rabs (x ^ x0)) b).x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
Rabs (x ^ n) >= Rabs (x ^ x0)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
Rabs (x ^ x0) >= b
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
exists N : nat, INR N >= b * / (Rabs x - 1)
  apply Rle_ge; apply Power_monotonic; assumption.x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
Rabs (x ^ x0) >= b
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
exists N : nat, INR N >= b * / (Rabs x - 1)
  rewrite <- RPow_abs; cut (Rabs x = 1 + (Rabs x - 1)).x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
Rabs x = 1 + (Rabs x - 1) -> Rabs x ^ x0 >= b
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
Rabs x = 1 + (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
exists N : nat, INR N >= b * / (Rabs x - 1)
  intro; rewrite H3;
    apply (Rge_trans ((1 + (Rabs x - 1)) ^ x0) (1 + INR x0 * (Rabs x - 1)) b).x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
H3:Rabs x = 1 + (Rabs x - 1)
(1 + (Rabs x - 1)) ^ x0 >= 1 + INR x0 * (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
H3:Rabs x = 1 + (Rabs x - 1)
1 + INR x0 * (Rabs x - 1) >= b
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
Rabs x = 1 + (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
exists N : nat, INR N >= b * / (Rabs x - 1)
  apply Rle_ge; apply poly; fold (Rabs x - 1 > 0); apply Rgt_minus;
    assumption.x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
H3:Rabs x = 1 + (Rabs x - 1)
1 + INR x0 * (Rabs x - 1) >= b
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
Rabs x = 1 + (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
exists N : nat, INR N >= b * / (Rabs x - 1)
  apply (Rge_trans (1 + INR x0 * (Rabs x - 1)) (INR x0 * (Rabs x - 1)) b).x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
H3:Rabs x = 1 + (Rabs x - 1)
1 + INR x0 * (Rabs x - 1) >= INR x0 * (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
H3:Rabs x = 1 + (Rabs x - 1)
INR x0 * (Rabs x - 1) >= b
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
Rabs x = 1 + (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
exists N : nat, INR N >= b * / (Rabs x - 1)
  apply Rle_ge; apply Rlt_le; rewrite (Rplus_comm 1 (INR x0 * (Rabs x - 1)));
    pattern (INR x0 * (Rabs x - 1)) at 1;
      rewrite <- (let (H1, H2) := Rplus_ne (INR x0 * (Rabs x - 1)) in H1);
        apply Rplus_lt_compat_l; apply Rlt_0_1.x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
H3:Rabs x = 1 + (Rabs x - 1)
INR x0 * (Rabs x - 1) >= b
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
Rabs x = 1 + (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
exists N : nat, INR N >= b * / (Rabs x - 1)
  cut (b = b * / (Rabs x - 1) * (Rabs x - 1)).x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
H3:Rabs x = 1 + (Rabs x - 1)
b = b * / (Rabs x - 1) * (Rabs x - 1) ->
INR x0 * (Rabs x - 1) >= b
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
H3:Rabs x = 1 + (Rabs x - 1)
b = b * / (Rabs x - 1) * (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
Rabs x = 1 + (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
exists N : nat, INR N >= b * / (Rabs x - 1)
  intros; rewrite H4; apply Rmult_ge_compat_r.x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
H3:Rabs x = 1 + (Rabs x - 1)
H4:b = b * / (Rabs x - 1) * (Rabs x - 1)
Rabs x - 1 >= 0
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
H3:Rabs x = 1 + (Rabs x - 1)
H4:b = b * / (Rabs x - 1) * (Rabs x - 1)
INR x0 >= b * / (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
H3:Rabs x = 1 + (Rabs x - 1)
b = b * / (Rabs x - 1) * (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
Rabs x = 1 + (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
exists N : nat, INR N >= b * / (Rabs x - 1)
  apply Rge_minus; unfold Rge; left; assumption.x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
H3:Rabs x = 1 + (Rabs x - 1)
H4:b = b * / (Rabs x - 1) * (Rabs x - 1)
INR x0 >= b * / (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
H3:Rabs x = 1 + (Rabs x - 1)
b = b * / (Rabs x - 1) * (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
Rabs x = 1 + (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
exists N : nat, INR N >= b * / (Rabs x - 1)
  assumption.x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
H3:Rabs x = 1 + (Rabs x - 1)
b = b * / (Rabs x - 1) * (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
Rabs x = 1 + (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
exists N : nat, INR N >= b * / (Rabs x - 1)
  rewrite Rmult_assoc; rewrite Rinv_l.x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
H3:Rabs x = 1 + (Rabs x - 1)
b = b * 1
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
H3:Rabs x = 1 + (Rabs x - 1)
Rabs x - 1 <> 0
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
Rabs x = 1 + (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
exists N : nat, INR N >= b * / (Rabs x - 1)
  ring.x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
H3:Rabs x = 1 + (Rabs x - 1)
Rabs x - 1 <> 0
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
Rabs x = 1 + (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
exists N : nat, INR N >= b * / (Rabs x - 1)
  apply Rlt_dichotomy_converse; right; apply Rgt_minus; assumption.x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
x0:nat
H1:INR x0 >= b * / (Rabs x - 1)
n:nat
H2:(n >= x0)%nat
Rabs x = 1 + (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
exists N : nat, INR N >= b * / (Rabs x - 1)
  ring.x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
exists N : nat, INR N >= b * / (Rabs x - 1)
  cut ((0 <= up (b * / (Rabs x - 1)))%Z \/ (up (b * / (Rabs x - 1)) <= 0)%Z).x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
(0 <= up (b * / (Rabs x - 1)))%Z \/
(up (b * / (Rabs x - 1)) <= 0)%Z ->
exists N : nat, INR N >= b * / (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
(0 <= up (b * / (Rabs x - 1)))%Z \/
(up (b * / (Rabs x - 1)) <= 0)%Z
  intros; elim H1; intro.x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
H1:(0 <= up (b * / (Rabs x - 1)))%Z \/
(up (b * / (Rabs x - 1)) <= 0)%Z
H2:(0 <= up (b * / (Rabs x - 1)))%Z
exists N : nat, INR N >= b * / (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
H1:(0 <= up (b * / (Rabs x - 1)))%Z \/
(up (b * / (Rabs x - 1)) <= 0)%Z
H2:(up (b * / (Rabs x - 1)) <= 0)%Z
exists N : nat, INR N >= b * / (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
(0 <= up (b * / (Rabs x - 1)))%Z \/
(up (b * / (Rabs x - 1)) <= 0)%Z
  elim (IZN (up (b * / (Rabs x - 1))) H2); intros; exists x0;
    apply
      (Rge_trans (INR x0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))).x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
H1:(0 <= up (b * / (Rabs x - 1)))%Z \/
(up (b * / (Rabs x - 1)) <= 0)%Z
H2:(0 <= up (b * / (Rabs x - 1)))%Z
x0:nat
H3:up (b * / (Rabs x - 1)) = Z.of_nat x0
INR x0 >= IZR (up (b * / (Rabs x - 1)))
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
H1:(0 <= up (b * / (Rabs x - 1)))%Z \/
(up (b * / (Rabs x - 1)) <= 0)%Z
H2:(0 <= up (b * / (Rabs x - 1)))%Z
x0:nat
H3:up (b * / (Rabs x - 1)) = Z.of_nat x0
IZR (up (b * / (Rabs x - 1))) >= b * / (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
H1:(0 <= up (b * / (Rabs x - 1)))%Z \/
(up (b * / (Rabs x - 1)) <= 0)%Z
H2:(up (b * / (Rabs x - 1)) <= 0)%Z
exists N : nat, INR N >= b * / (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
(0 <= up (b * / (Rabs x - 1)))%Z \/
(up (b * / (Rabs x - 1)) <= 0)%Z
  rewrite INR_IZR_INZ; apply IZR_ge; omega.x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
H1:(0 <= up (b * / (Rabs x - 1)))%Z \/
(up (b * / (Rabs x - 1)) <= 0)%Z
H2:(0 <= up (b * / (Rabs x - 1)))%Z
x0:nat
H3:up (b * / (Rabs x - 1)) = Z.of_nat x0
IZR (up (b * / (Rabs x - 1))) >= b * / (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
H1:(0 <= up (b * / (Rabs x - 1)))%Z \/
(up (b * / (Rabs x - 1)) <= 0)%Z
H2:(up (b * / (Rabs x - 1)) <= 0)%Z
exists N : nat, INR N >= b * / (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
(0 <= up (b * / (Rabs x - 1)))%Z \/
(up (b * / (Rabs x - 1)) <= 0)%Z
  unfold Rge; left; assumption.x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
H1:(0 <= up (b * / (Rabs x - 1)))%Z \/
(up (b * / (Rabs x - 1)) <= 0)%Z
H2:(up (b * / (Rabs x - 1)) <= 0)%Z
exists N : nat, INR N >= b * / (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
(0 <= up (b * / (Rabs x - 1)))%Z \/
(up (b * / (Rabs x - 1)) <= 0)%Z
  exists 0%nat;
    apply
      (Rge_trans (INR 0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))).x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
H1:(0 <= up (b * / (Rabs x - 1)))%Z \/
(up (b * / (Rabs x - 1)) <= 0)%Z
H2:(up (b * / (Rabs x - 1)) <= 0)%Z
INR 0 >= IZR (up (b * / (Rabs x - 1)))
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
H1:(0 <= up (b * / (Rabs x - 1)))%Z \/
(up (b * / (Rabs x - 1)) <= 0)%Z
H2:(up (b * / (Rabs x - 1)) <= 0)%Z
IZR (up (b * / (Rabs x - 1))) >= b * / (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
(0 <= up (b * / (Rabs x - 1)))%Z \/
(up (b * / (Rabs x - 1)) <= 0)%Z
  rewrite INR_IZR_INZ; apply IZR_ge; simpl; omega.x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
H1:(0 <= up (b * / (Rabs x - 1)))%Z \/
(up (b * / (Rabs x - 1)) <= 0)%Z
H2:(up (b * / (Rabs x - 1)) <= 0)%Z
IZR (up (b * / (Rabs x - 1))) >= b * / (Rabs x - 1)
x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
(0 <= up (b * / (Rabs x - 1)))%Z \/
(up (b * / (Rabs x - 1)) <= 0)%Z
  unfold Rge; left; assumption.x:R
H:Rabs x > 1
b:R
H0:IZR (up (b * / (Rabs x - 1))) >
b * / (Rabs x - 1)
(0 <= up (b * / (Rabs x - 1)))%Z \/
(up (b * / (Rabs x - 1)) <= 0)%Z
  omega.
Qed.

Lemma pow_ne_zero : forall n:nat, n <> 0%nat -> 0 ^ n = 0.forall n : nat, n <> 0%nat -> 0 ^ n = 0
Proof.forall n : nat, n <> 0%nat -> 0 ^ n = 0
  simple induction n.n:nat
0%nat <> 0%nat -> 0 ^ 0 = 0
n:nat
forall n0 : nat,
(n0 <> 0%nat -> 0 ^ n0 = 0) ->
S n0 <> 0%nat -> 0 ^ S n0 = 0
  simpl; auto.n:nat
0%nat <> 0%nat -> 1 = 0
n:nat
forall n0 : nat,
(n0 <> 0%nat -> 0 ^ n0 = 0) ->
S n0 <> 0%nat -> 0 ^ S n0 = 0
  intros; elim H; reflexivity.n:nat
forall n0 : nat,
(n0 <> 0%nat -> 0 ^ n0 = 0) ->
S n0 <> 0%nat -> 0 ^ S n0 = 0
  intros; simpl; apply Rmult_0_l.
Qed.

Lemma Rinv_pow : forall (x:R) (n:nat), x <> 0 -> / x ^ n = (/ x) ^ n.forall (x : R) (n : nat),
x <> 0 -> / x ^ n = (/ x) ^ n
Proof.forall (x : R) (n : nat),
x <> 0 -> / x ^ n = (/ x) ^ n
  intros; elim n; simpl.x:R
n:nat
H:x <> 0
/ 1 = 1
x:R
n:nat
H:x <> 0
forall n0 : nat,
/ x ^ n0 = (/ x) ^ n0 ->
/ (x * x ^ n0) = / x * (/ x) ^ n0
  apply Rinv_1.x:R
n:nat
H:x <> 0
forall n0 : nat,
/ x ^ n0 = (/ x) ^ n0 ->
/ (x * x ^ n0) = / x * (/ x) ^ n0
  intro m; intro; rewrite Rinv_mult_distr.x:R
n:nat
H:x <> 0
m:nat
H0:/ x ^ m = (/ x) ^ m
/ x * / x ^ m = / x * (/ x) ^ m
x:R
n:nat
H:x <> 0
m:nat
H0:/ x ^ m = (/ x) ^ m
x <> 0
x:R
n:nat
H:x <> 0
m:nat
H0:/ x ^ m = (/ x) ^ m
x ^ m <> 0
  rewrite H0; reflexivity; assumption.x:R
n:nat
H:x <> 0
m:nat
H0:/ x ^ m = (/ x) ^ m
x <> 0
x:R
n:nat
H:x <> 0
m:nat
H0:/ x ^ m = (/ x) ^ m
x ^ m <> 0
  assumption.x:R
n:nat
H:x <> 0
m:nat
H0:/ x ^ m = (/ x) ^ m
x ^ m <> 0
  apply pow_nonzero; assumption.
Qed.

Lemma pow_lt_1_zero :
  forall x:R,
    Rabs x < 1 ->
    forall y:R,
      0 < y ->
      exists N : nat, (forall n:nat, (n >= N)%nat -> Rabs (x ^ n) < y).forall x : R,
Rabs x < 1 ->
forall y : R,
0 < y ->
exists N : nat,
  forall n : nat, (n >= N)%nat -> Rabs (x ^ n) < y
Proof.forall x : R,
Rabs x < 1 ->
forall y : R,
0 < y ->
exists N : nat,
  forall n : nat, (n >= N)%nat -> Rabs (x ^ n) < y
  intros; elim (Req_dec x 0); intro.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x = 0
exists N : nat,
  forall n : nat, (n >= N)%nat -> Rabs (x ^ n) < y
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
exists N : nat,
  forall n : nat, (n >= N)%nat -> Rabs (x ^ n) < y
  exists 1%nat; rewrite H1; intros n GE; rewrite pow_ne_zero.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x = 0
n:nat
GE:(n >= 1)%nat
Rabs 0 < y
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x = 0
n:nat
GE:(n >= 1)%nat
n <> 0%nat
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
exists N : nat,
  forall n : nat, (n >= N)%nat -> Rabs (x ^ n) < y
  rewrite Rabs_R0; assumption.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x = 0
n:nat
GE:(n >= 1)%nat
n <> 0%nat
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
exists N : nat,
  forall n : nat, (n >= N)%nat -> Rabs (x ^ n) < y
  inversion GE; auto.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
exists N : nat,
  forall n : nat, (n >= N)%nat -> Rabs (x ^ n) < y
  cut (Rabs (/ x) > 1).x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1 ->
exists N : nat,
  forall n : nat, (n >= N)%nat -> Rabs (x ^ n) < y
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  intros; elim (Pow_x_infinity (/ x) H2 (/ y + 1)); intros N.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
(forall n : nat,
 (n >= N)%nat -> Rabs ((/ x) ^ n) >= / y + 1) ->
exists N0 : nat,
  forall n : nat, (n >= N0)%nat -> Rabs (x ^ n) < y
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  exists N; intros; rewrite <- (Rinv_involutive y).x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
Rabs (x ^ n) < / / y
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  rewrite <- (Rinv_involutive (Rabs (x ^ n))).x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
/ / Rabs (x ^ n) < / / y
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
Rabs (x ^ n) <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  apply Rinv_lt_contravar.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
0 < / y * / Rabs (x ^ n)
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
/ y < / Rabs (x ^ n)
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
Rabs (x ^ n) <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  apply Rmult_lt_0_compat.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
0 < / y
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
0 < / Rabs (x ^ n)
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
/ y < / Rabs (x ^ n)
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
Rabs (x ^ n) <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  apply Rinv_0_lt_compat.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
0 < y
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
0 < / Rabs (x ^ n)
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
/ y < / Rabs (x ^ n)
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
Rabs (x ^ n) <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  assumption.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
0 < / Rabs (x ^ n)
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
/ y < / Rabs (x ^ n)
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
Rabs (x ^ n) <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  apply Rinv_0_lt_compat.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
0 < Rabs (x ^ n)
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
/ y < / Rabs (x ^ n)
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
Rabs (x ^ n) <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  apply Rabs_pos_lt.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x ^ n <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
/ y < / Rabs (x ^ n)
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
Rabs (x ^ n) <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  apply pow_nonzero.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
/ y < / Rabs (x ^ n)
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
Rabs (x ^ n) <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  assumption.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
/ y < / Rabs (x ^ n)
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
Rabs (x ^ n) <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  rewrite <- Rabs_Rinv.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
/ y < Rabs (/ x ^ n)
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x ^ n <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
Rabs (x ^ n) <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  rewrite Rinv_pow.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
/ y < Rabs ((/ x) ^ n)
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x ^ n <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
Rabs (x ^ n) <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  apply (Rlt_le_trans (/ y) (/ y + 1) (Rabs ((/ x) ^ n))).x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
/ y < / y + 1
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
/ y + 1 <= Rabs ((/ x) ^ n)
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x ^ n <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
Rabs (x ^ n) <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  pattern (/ y) at 1.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
(fun r : R => r < / y + 1) (/ y)
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
/ y + 1 <= Rabs ((/ x) ^ n)
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x ^ n <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
Rabs (x ^ n) <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  rewrite <- (let (H1, H2) := Rplus_ne (/ y) in H1).x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
/ y + 0 < / y + 1
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
/ y + 1 <= Rabs ((/ x) ^ n)
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x ^ n <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
Rabs (x ^ n) <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  apply Rplus_lt_compat_l.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
0 < 1
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
/ y + 1 <= Rabs ((/ x) ^ n)
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x ^ n <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
Rabs (x ^ n) <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  apply Rlt_0_1.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
/ y + 1 <= Rabs ((/ x) ^ n)
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x ^ n <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
Rabs (x ^ n) <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  apply Rge_le.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
Rabs ((/ x) ^ n) >= / y + 1
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x ^ n <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
Rabs (x ^ n) <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  apply H3.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
(n >= N)%nat
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x ^ n <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
Rabs (x ^ n) <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  assumption.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x ^ n <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
Rabs (x ^ n) <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  assumption.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x ^ n <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
Rabs (x ^ n) <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  apply pow_nonzero.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
Rabs (x ^ n) <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  assumption.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
Rabs (x ^ n) <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  apply Rabs_no_R0.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x ^ n <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  apply pow_nonzero.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
x <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  assumption.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  apply Rlt_dichotomy_converse.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
H2:Rabs (/ x) > 1
N:nat
H3:forall n0 : nat,
(n0 >= N)%nat -> Rabs ((/ x) ^ n0) >= / y + 1
n:nat
H4:(n >= N)%nat
y < 0 \/ y > 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  right; unfold Rgt; assumption.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > 1
  rewrite <- (Rinv_involutive 1).x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs (/ x) > / / 1
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
1 <> 0
  rewrite Rabs_Rinv.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
/ Rabs x > / / 1
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
x <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
1 <> 0
  unfold Rgt; apply Rinv_lt_contravar.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
0 < Rabs x * / 1
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs x < / 1
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
x <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
1 <> 0
  apply Rmult_lt_0_compat.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
0 < Rabs x
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
0 < / 1
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs x < / 1
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
x <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
1 <> 0
  apply Rabs_pos_lt.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
x <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
0 < / 1
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs x < / 1
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
x <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
1 <> 0
  assumption.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
0 < / 1
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs x < / 1
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
x <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
1 <> 0
  rewrite Rinv_1; apply Rlt_0_1.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
Rabs x < / 1
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
x <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
1 <> 0
  rewrite Rinv_1; assumption.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
x <> 0
x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
1 <> 0
  assumption.x:R
H:Rabs x < 1
y:R
H0:0 < y
H1:x <> 0
1 <> 0
  red; intro; apply R1_neq_R0; assumption.
Qed.

Lemma pow_R1 : forall (r:R) (n:nat), r ^ n = 1 -> Rabs r = 1 \/ n = 0%nat.forall (r : R) (n : nat),
r ^ n = 1 -> Rabs r = 1 \/ n = 0%nat
Proof.forall (r : R) (n : nat),
r ^ n = 1 -> Rabs r = 1 \/ n = 0%nat
  intros r n H'.r:R
n:nat
H':r ^ n = 1
Rabs r = 1 \/ n = 0%nat
  case (Req_dec (Rabs r) 1); auto; intros H'1.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
Rabs r = 1 \/ n = 0%nat
  case (Rdichotomy _ _ H'1); intros H'2.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
Rabs r = 1 \/ n = 0%nat
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
Rabs r = 1 \/ n = 0%nat
  generalize H'; case n; auto.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
forall n0 : nat,
r ^ S n0 = 1 -> Rabs r = 1 \/ S n0 = 0%nat
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
Rabs r = 1 \/ n = 0%nat
  intros n0 H'0.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
Rabs r = 1 \/ S n0 = 0%nat
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
Rabs r = 1 \/ n = 0%nat
  cut (r <> 0); [ intros Eq1 | idtac ].r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Rabs r = 1 \/ S n0 = 0%nat
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
r <> 0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
Rabs r = 1 \/ n = 0%nat
  cut (Rabs r <> 0); [ intros Eq2 | apply Rabs_no_R0 ]; auto.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Eq2:Rabs r <> 0
Rabs r = 1 \/ S n0 = 0%nat
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
r <> 0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
Rabs r = 1 \/ n = 0%nat
  absurd (Rabs (/ r) ^ 0 < Rabs (/ r) ^ S n0); auto.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Eq2:Rabs r <> 0
~ Rabs (/ r) ^ 0 < Rabs (/ r) ^ S n0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Eq2:Rabs r <> 0
Rabs (/ r) ^ 0 < Rabs (/ r) ^ S n0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
r <> 0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
Rabs r = 1 \/ n = 0%nat
  replace (Rabs (/ r) ^ S n0) with 1.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Eq2:Rabs r <> 0
~ Rabs (/ r) ^ 0 < 1
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Eq2:Rabs r <> 0
1 = Rabs (/ r) ^ S n0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Eq2:Rabs r <> 0
Rabs (/ r) ^ 0 < Rabs (/ r) ^ S n0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
r <> 0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
Rabs r = 1 \/ n = 0%nat
  simpl; apply Rlt_irrefl; auto.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Eq2:Rabs r <> 0
1 = Rabs (/ r) ^ S n0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Eq2:Rabs r <> 0
Rabs (/ r) ^ 0 < Rabs (/ r) ^ S n0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
r <> 0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
Rabs r = 1 \/ n = 0%nat
  rewrite Rabs_Rinv; auto.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Eq2:Rabs r <> 0
1 = (/ Rabs r) ^ S n0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Eq2:Rabs r <> 0
Rabs (/ r) ^ 0 < Rabs (/ r) ^ S n0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
r <> 0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
Rabs r = 1 \/ n = 0%nat
  rewrite <- Rinv_pow; auto.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Eq2:Rabs r <> 0
1 = / Rabs r ^ S n0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Eq2:Rabs r <> 0
Rabs (/ r) ^ 0 < Rabs (/ r) ^ S n0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
r <> 0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
Rabs r = 1 \/ n = 0%nat
  rewrite RPow_abs; auto.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Eq2:Rabs r <> 0
1 = / Rabs (r ^ S n0)
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Eq2:Rabs r <> 0
Rabs (/ r) ^ 0 < Rabs (/ r) ^ S n0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
r <> 0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
Rabs r = 1 \/ n = 0%nat
  rewrite H'0; rewrite Rabs_right; auto with real rorders.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Eq2:Rabs r <> 0
Rabs (/ r) ^ 0 < Rabs (/ r) ^ S n0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
r <> 0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
Rabs r = 1 \/ n = 0%nat
  apply Rlt_pow; auto with arith.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Eq2:Rabs r <> 0
1 < Rabs (/ r)
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
r <> 0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
Rabs r = 1 \/ n = 0%nat
  rewrite Rabs_Rinv; auto.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Eq2:Rabs r <> 0
1 < / Rabs r
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
r <> 0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
Rabs r = 1 \/ n = 0%nat
  apply Rmult_lt_reg_l with (r := Rabs r).r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Eq2:Rabs r <> 0
0 < Rabs r
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Eq2:Rabs r <> 0
Rabs r * 1 < Rabs r * / Rabs r
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
r <> 0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
Rabs r = 1 \/ n = 0%nat
  case (Rabs_pos r); auto.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Eq2:Rabs r <> 0
0 = Rabs r -> 0 < Rabs r
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Eq2:Rabs r <> 0
Rabs r * 1 < Rabs r * / Rabs r
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
r <> 0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
Rabs r = 1 \/ n = 0%nat
  intros H'3; case Eq2; auto.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Eq2:Rabs r <> 0
Rabs r * 1 < Rabs r * / Rabs r
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
r <> 0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
Rabs r = 1 \/ n = 0%nat
  rewrite Rmult_1_r; rewrite Rinv_r; auto with real.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
r <> 0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
Rabs r = 1 \/ n = 0%nat
  red; intro; absurd (r ^ S n0 = 1); auto.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r < 1
n0:nat
H'0:r ^ S n0 = 1
H:r = 0
r ^ S n0 <> 1
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
Rabs r = 1 \/ n = 0%nat
  simpl; rewrite H; rewrite Rmult_0_l; auto with real.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
Rabs r = 1 \/ n = 0%nat
  generalize H'; case n; auto.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
forall n0 : nat,
r ^ S n0 = 1 -> Rabs r = 1 \/ S n0 = 0%nat
  intros n0 H'0.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
n0:nat
H'0:r ^ S n0 = 1
Rabs r = 1 \/ S n0 = 0%nat
  cut (r <> 0); [ intros Eq1 | auto with real ].r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Rabs r = 1 \/ S n0 = 0%nat
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
n0:nat
H'0:r ^ S n0 = 1
r <> 0
  cut (Rabs r <> 0); [ intros Eq2 | apply Rabs_no_R0 ]; auto.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Eq2:Rabs r <> 0
Rabs r = 1 \/ S n0 = 0%nat
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
n0:nat
H'0:r ^ S n0 = 1
r <> 0
  absurd (Rabs r ^ 0 < Rabs r ^ S n0); auto with real arith.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
n0:nat
H'0:r ^ S n0 = 1
Eq1:r <> 0
Eq2:Rabs r <> 0
~ Rabs r ^ 0 < Rabs r ^ S n0
r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
n0:nat
H'0:r ^ S n0 = 1
r <> 0
  repeat rewrite RPow_abs; rewrite H'0; simpl; auto with real.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
n0:nat
H'0:r ^ S n0 = 1
r <> 0
  red; intro; absurd (r ^ S n0 = 1); auto.r:R
n:nat
H':r ^ n = 1
H'1:Rabs r <> 1
H'2:Rabs r > 1
n0:nat
H'0:r ^ S n0 = 1
H:r = 0
r ^ S n0 <> 1
  simpl; rewrite H; rewrite Rmult_0_l; auto with real.
Qed.

Lemma pow_Rsqr : forall (x:R) (n:nat), x ^ (2 * n) = Rsqr x ^ n.forall (x : R) (n : nat), x ^ (2 * n) = x² ^ n
Proof.forall (x : R) (n : nat), x ^ (2 * n) = x² ^ n
  intros; induction  n as [| n Hrecn].x:R
x ^ (2 * 0) = x² ^ 0
x:R
n:nat
Hrecn:x ^ (2 * n) = x² ^ n
x ^ (2 * S n) = x² ^ S n
  reflexivity.x:R
n:nat
Hrecn:x ^ (2 * n) = x² ^ n
x ^ (2 * S n) = x² ^ S n
  replace (2 * S n)%nat with (S (S (2 * n))).x:R
n:nat
Hrecn:x ^ (2 * n) = x² ^ n
x ^ S (S (2 * n)) = x² ^ S n
x:R
n:nat
Hrecn:x ^ (2 * n) = x² ^ n
S (S (2 * n)) = (2 * S n)%nat
  replace (x ^ S (S (2 * n))) with (x * x * x ^ (2 * n)).x:R
n:nat
Hrecn:x ^ (2 * n) = x² ^ n
x * x * x ^ (2 * n) = x² ^ S n
x:R
n:nat
Hrecn:x ^ (2 * n) = x² ^ n
x * x * x ^ (2 * n) = x ^ S (S (2 * n))
x:R
n:nat
Hrecn:x ^ (2 * n) = x² ^ n
S (S (2 * n)) = (2 * S n)%nat
  rewrite Hrecn; reflexivity.x:R
n:nat
Hrecn:x ^ (2 * n) = x² ^ n
x * x * x ^ (2 * n) = x ^ S (S (2 * n))
x:R
n:nat
Hrecn:x ^ (2 * n) = x² ^ n
S (S (2 * n)) = (2 * S n)%nat
  simpl; ring.x:R
n:nat
Hrecn:x ^ (2 * n) = x² ^ n
S (S (2 * n)) = (2 * S n)%nat
  ring.
Qed.

Lemma pow_le : forall (a:R) (n:nat), 0 <= a -> 0 <= a ^ n.forall (a : R) (n : nat), 0 <= a -> 0 <= a ^ n
Proof.forall (a : R) (n : nat), 0 <= a -> 0 <= a ^ n
  intros; induction  n as [| n Hrecn].a:R
H:0 <= a
0 <= a ^ 0
a:R
n:nat
H:0 <= a
Hrecn:0 <= a ^ n
0 <= a ^ S n
  simpl; left; apply Rlt_0_1.a:R
n:nat
H:0 <= a
Hrecn:0 <= a ^ n
0 <= a ^ S n
  simpl; apply Rmult_le_pos; assumption.
Qed.

(**********)
Lemma pow_1_even : forall n:nat, (-1) ^ (2 * n) = 1.forall n : nat, (-1) ^ (2 * n) = 1
Proof.forall n : nat, (-1) ^ (2 * n) = 1
  intro; induction  n as [| n Hrecn].(-1) ^ (2 * 0) = 1
n:nat
Hrecn:(-1) ^ (2 * n) = 1
(-1) ^ (2 * S n) = 1
  reflexivity.n:nat
Hrecn:(-1) ^ (2 * n) = 1
(-1) ^ (2 * S n) = 1
  replace (2 * S n)%nat with (2 + 2 * n)%nat by ring.n:nat
Hrecn:(-1) ^ (2 * n) = 1
(-1) ^ (2 + 2 * n) = 1
  rewrite pow_add; rewrite Hrecn; simpl; ring.
Qed.

(**********)
Lemma pow_1_odd : forall n:nat, (-1) ^ S (2 * n) = -1.forall n : nat, (-1) ^ S (2 * n) = -1
Proof.forall n : nat, (-1) ^ S (2 * n) = -1
  intro; replace (S (2 * n)) with (2 * n + 1)%nat by ring.n:nat
(-1) ^ (2 * n + 1) = -1
  rewrite pow_add; rewrite pow_1_even; simpl; ring.
Qed.

(**********)
Lemma pow_1_abs : forall n:nat, Rabs ((-1) ^ n) = 1.forall n : nat, Rabs ((-1) ^ n) = 1
Proof.forall n : nat, Rabs ((-1) ^ n) = 1
  intro; induction  n as [| n Hrecn].Rabs ((-1) ^ 0) = 1
n:nat
Hrecn:Rabs ((-1) ^ n) = 1
Rabs ((-1) ^ S n) = 1
  simpl; apply Rabs_R1.n:nat
Hrecn:Rabs ((-1) ^ n) = 1
Rabs ((-1) ^ S n) = 1
  replace (S n) with (n + 1)%nat; [ rewrite pow_add | ring ].n:nat
Hrecn:Rabs ((-1) ^ n) = 1
Rabs ((-1) ^ n * (-1) ^ 1) = 1
  rewrite Rabs_mult.n:nat
Hrecn:Rabs ((-1) ^ n) = 1
Rabs ((-1) ^ n) * Rabs ((-1) ^ 1) = 1
  rewrite Hrecn; rewrite Rmult_1_l; simpl; rewrite Rmult_1_r.n:nat
Hrecn:Rabs ((-1) ^ n) = 1
Rabs (-1) = 1
  change (-1) with (-(1)).n:nat
Hrecn:Rabs ((-1) ^ n) = 1
Rabs (- (1)) = 1
  rewrite Rabs_Ropp; apply Rabs_R1.
Qed.

Lemma pow_mult : forall (x:R) (n1 n2:nat), x ^ (n1 * n2) = (x ^ n1) ^ n2.forall (x : R) (n1 n2 : nat),
x ^ (n1 * n2) = (x ^ n1) ^ n2
Proof.forall (x : R) (n1 n2 : nat),
x ^ (n1 * n2) = (x ^ n1) ^ n2
  intros; induction  n2 as [| n2 Hrecn2].x:R
n1:nat
x ^ (n1 * 0) = (x ^ n1) ^ 0
x:R
n1, n2:nat
Hrecn2:x ^ (n1 * n2) = (x ^ n1) ^ n2
x ^ (n1 * S n2) = (x ^ n1) ^ S n2
  simpl; replace (n1 * 0)%nat with 0%nat; [ reflexivity | ring ].x:R
n1, n2:nat
Hrecn2:x ^ (n1 * n2) = (x ^ n1) ^ n2
x ^ (n1 * S n2) = (x ^ n1) ^ S n2
  replace (n1 * S n2)%nat with (n1 * n2 + n1)%nat.x:R
n1, n2:nat
Hrecn2:x ^ (n1 * n2) = (x ^ n1) ^ n2
x ^ (n1 * n2 + n1) = (x ^ n1) ^ S n2
x:R
n1, n2:nat
Hrecn2:x ^ (n1 * n2) = (x ^ n1) ^ n2
(n1 * n2 + n1)%nat = (n1 * S n2)%nat
  replace (S n2) with (n2 + 1)%nat by ring.x:R
n1, n2:nat
Hrecn2:x ^ (n1 * n2) = (x ^ n1) ^ n2
x ^ (n1 * n2 + n1) = (x ^ n1) ^ (n2 + 1)
x:R
n1, n2:nat
Hrecn2:x ^ (n1 * n2) = (x ^ n1) ^ n2
(n1 * n2 + n1)%nat = (n1 * S n2)%nat
  do 2 rewrite pow_add.x:R
n1, n2:nat
Hrecn2:x ^ (n1 * n2) = (x ^ n1) ^ n2
x ^ (n1 * n2) * x ^ n1 = (x ^ n1) ^ n2 * (x ^ n1) ^ 1
x:R
n1, n2:nat
Hrecn2:x ^ (n1 * n2) = (x ^ n1) ^ n2
(n1 * n2 + n1)%nat = (n1 * S n2)%nat
  rewrite Hrecn2.x:R
n1, n2:nat
Hrecn2:x ^ (n1 * n2) = (x ^ n1) ^ n2
(x ^ n1) ^ n2 * x ^ n1 = (x ^ n1) ^ n2 * (x ^ n1) ^ 1
x:R
n1, n2:nat
Hrecn2:x ^ (n1 * n2) = (x ^ n1) ^ n2
(n1 * n2 + n1)%nat = (n1 * S n2)%nat
  simpl.x:R
n1, n2:nat
Hrecn2:x ^ (n1 * n2) = (x ^ n1) ^ n2
(x ^ n1) ^ n2 * x ^ n1 = (x ^ n1) ^ n2 * (x ^ n1 * 1)
x:R
n1, n2:nat
Hrecn2:x ^ (n1 * n2) = (x ^ n1) ^ n2
(n1 * n2 + n1)%nat = (n1 * S n2)%nat
  ring.x:R
n1, n2:nat
Hrecn2:x ^ (n1 * n2) = (x ^ n1) ^ n2
(n1 * n2 + n1)%nat = (n1 * S n2)%nat
  ring.
Qed.

Lemma pow_incr : forall (x y:R) (n:nat), 0 <= x <= y -> x ^ n <= y ^ n.forall (x y : R) (n : nat),
0 <= x <= y -> x ^ n <= y ^ n
Proof.forall (x y : R) (n : nat),
0 <= x <= y -> x ^ n <= y ^ n
  intros.x, y:R
n:nat
H:0 <= x <= y
x ^ n <= y ^ n
  induction  n as [| n Hrecn].x, y:R
H:0 <= x <= y
x ^ 0 <= y ^ 0
x, y:R
n:nat
H:0 <= x <= y
Hrecn:x ^ n <= y ^ n
x ^ S n <= y ^ S n
  right; reflexivity.x, y:R
n:nat
H:0 <= x <= y
Hrecn:x ^ n <= y ^ n
x ^ S n <= y ^ S n
  simpl.x, y:R
n:nat
H:0 <= x <= y
Hrecn:x ^ n <= y ^ n
x * x ^ n <= y * y ^ n
  elim H; intros.x, y:R
n:nat
H:0 <= x <= y
Hrecn:x ^ n <= y ^ n
H0:0 <= x
H1:x <= y
x * x ^ n <= y * y ^ n
  apply Rle_trans with (y * x ^ n).x, y:R
n:nat
H:0 <= x <= y
Hrecn:x ^ n <= y ^ n
H0:0 <= x
H1:x <= y
x * x ^ n <= y * x ^ n
x, y:R
n:nat
H:0 <= x <= y
Hrecn:x ^ n <= y ^ n
H0:0 <= x
H1:x <= y
y * x ^ n <= y * y ^ n
  do 2 rewrite <- (Rmult_comm (x ^ n)).x, y:R
n:nat
H:0 <= x <= y
Hrecn:x ^ n <= y ^ n
H0:0 <= x
H1:x <= y
x ^ n * x <= x ^ n * y
x, y:R
n:nat
H:0 <= x <= y
Hrecn:x ^ n <= y ^ n
H0:0 <= x
H1:x <= y
y * x ^ n <= y * y ^ n
  apply Rmult_le_compat_l.x, y:R
n:nat
H:0 <= x <= y
Hrecn:x ^ n <= y ^ n
H0:0 <= x
H1:x <= y
0 <= x ^ n
x, y:R
n:nat
H:0 <= x <= y
Hrecn:x ^ n <= y ^ n
H0:0 <= x
H1:x <= y
x <= y
x, y:R
n:nat
H:0 <= x <= y
Hrecn:x ^ n <= y ^ n
H0:0 <= x
H1:x <= y
y * x ^ n <= y * y ^ n
  apply pow_le; assumption.x, y:R
n:nat
H:0 <= x <= y
Hrecn:x ^ n <= y ^ n
H0:0 <= x
H1:x <= y
x <= y
x, y:R
n:nat
H:0 <= x <= y
Hrecn:x ^ n <= y ^ n
H0:0 <= x
H1:x <= y
y * x ^ n <= y * y ^ n
  assumption.x, y:R
n:nat
H:0 <= x <= y
Hrecn:x ^ n <= y ^ n
H0:0 <= x
H1:x <= y
y * x ^ n <= y * y ^ n
  apply Rmult_le_compat_l.x, y:R
n:nat
H:0 <= x <= y
Hrecn:x ^ n <= y ^ n
H0:0 <= x
H1:x <= y
0 <= y
x, y:R
n:nat
H:0 <= x <= y
Hrecn:x ^ n <= y ^ n
H0:0 <= x
H1:x <= y
x ^ n <= y ^ n
  apply Rle_trans with x; assumption.x, y:R
n:nat
H:0 <= x <= y
Hrecn:x ^ n <= y ^ n
H0:0 <= x
H1:x <= y
x ^ n <= y ^ n
  apply Hrecn.
Qed.

Lemma pow_R1_Rle : forall (x:R) (k:nat), 1 <= x -> 1 <= x ^ k.forall (x : R) (k : nat), 1 <= x -> 1 <= x ^ k
Proof.forall (x : R) (k : nat), 1 <= x -> 1 <= x ^ k
  intros.x:R
k:nat
H:1 <= x
1 <= x ^ k
  induction  k as [| k Hreck].x:R
H:1 <= x
1 <= x ^ 0
x:R
k:nat
H:1 <= x
Hreck:1 <= x ^ k
1 <= x ^ S k
  right; reflexivity.x:R
k:nat
H:1 <= x
Hreck:1 <= x ^ k
1 <= x ^ S k
  simpl.x:R
k:nat
H:1 <= x
Hreck:1 <= x ^ k
1 <= x * x ^ k
  apply Rle_trans with (x * 1).x:R
k:nat
H:1 <= x
Hreck:1 <= x ^ k
1 <= x * 1
x:R
k:nat
H:1 <= x
Hreck:1 <= x ^ k
x * 1 <= x * x ^ k
  rewrite Rmult_1_r; assumption.x:R
k:nat
H:1 <= x
Hreck:1 <= x ^ k
x * 1 <= x * x ^ k
  apply Rmult_le_compat_l.x:R
k:nat
H:1 <= x
Hreck:1 <= x ^ k
0 <= x
x:R
k:nat
H:1 <= x
Hreck:1 <= x ^ k
1 <= x ^ k
  left; apply Rlt_le_trans with 1; [ apply Rlt_0_1 | assumption ].x:R
k:nat
H:1 <= x
Hreck:1 <= x ^ k
1 <= x ^ k
  exact Hreck.
Qed.

Lemma Rle_pow :
  forall (x:R) (m n:nat), 1 <= x -> (m <= n)%nat -> x ^ m <= x ^ n.forall (x : R) (m n : nat),
1 <= x -> (m <= n)%nat -> x ^ m <= x ^ n
Proof.forall (x : R) (m n : nat),
1 <= x -> (m <= n)%nat -> x ^ m <= x ^ n
  intros.x:R
m, n:nat
H:1 <= x
H0:(m <= n)%nat
x ^ m <= x ^ n
  replace n with (n - m + m)%nat.x:R
m, n:nat
H:1 <= x
H0:(m <= n)%nat
x ^ m <= x ^ (n - m + m)
x:R
m, n:nat
H:1 <= x
H0:(m <= n)%nat
(n - m + m)%nat = n
  rewrite pow_add.x:R
m, n:nat
H:1 <= x
H0:(m <= n)%nat
x ^ m <= x ^ (n - m) * x ^ m
x:R
m, n:nat
H:1 <= x
H0:(m <= n)%nat
(n - m + m)%nat = n
  rewrite Rmult_comm.x:R
m, n:nat
H:1 <= x
H0:(m <= n)%nat
x ^ m <= x ^ m * x ^ (n - m)
x:R
m, n:nat
H:1 <= x
H0:(m <= n)%nat
(n - m + m)%nat = n
  pattern (x ^ m) at 1; rewrite <- Rmult_1_r.x:R
m, n:nat
H:1 <= x
H0:(m <= n)%nat
x ^ m * 1 <= x ^ m * x ^ (n - m)
x:R
m, n:nat
H:1 <= x
H0:(m <= n)%nat
(n - m + m)%nat = n
  apply Rmult_le_compat_l.x:R
m, n:nat
H:1 <= x
H0:(m <= n)%nat
0 <= x ^ m
x:R
m, n:nat
H:1 <= x
H0:(m <= n)%nat
1 <= x ^ (n - m)
x:R
m, n:nat
H:1 <= x
H0:(m <= n)%nat
(n - m + m)%nat = n
  apply pow_le; left; apply Rlt_le_trans with 1; [ apply Rlt_0_1 | assumption ].x:R
m, n:nat
H:1 <= x
H0:(m <= n)%nat
1 <= x ^ (n - m)
x:R
m, n:nat
H:1 <= x
H0:(m <= n)%nat
(n - m + m)%nat = n
  apply pow_R1_Rle; assumption.x:R
m, n:nat
H:1 <= x
H0:(m <= n)%nat
(n - m + m)%nat = n
  rewrite plus_comm.x:R
m, n:nat
H:1 <= x
H0:(m <= n)%nat
(m + (n - m))%nat = n
  symmetry ; apply le_plus_minus; assumption.
Qed.

Lemma pow1 : forall n:nat, 1 ^ n = 1.forall n : nat, 1 ^ n = 1
Proof.forall n : nat, 1 ^ n = 1
  intro; induction  n as [| n Hrecn].1 ^ 0 = 1
n:nat
Hrecn:1 ^ n = 1
1 ^ S n = 1
  reflexivity.n:nat
Hrecn:1 ^ n = 1
1 ^ S n = 1
  simpl; rewrite Hrecn; rewrite Rmult_1_r; reflexivity.
Qed.

Lemma pow_Rabs : forall (x:R) (n:nat), x ^ n <= Rabs x ^ n.forall (x : R) (n : nat), x ^ n <= Rabs x ^ n
Proof.forall (x : R) (n : nat), x ^ n <= Rabs x ^ n
  intros; induction  n as [| n Hrecn].x:R
x ^ 0 <= Rabs x ^ 0
x:R
n:nat
Hrecn:x ^ n <= Rabs x ^ n
x ^ S n <= Rabs x ^ S n
  right; reflexivity.x:R
n:nat
Hrecn:x ^ n <= Rabs x ^ n
x ^ S n <= Rabs x ^ S n
  simpl; destruct (Rcase_abs x) as [Hlt|Hle].x:R
n:nat
Hrecn:x ^ n <= Rabs x ^ n
Hlt:x < 0
x * x ^ n <= Rabs x * Rabs x ^ n
x:R
n:nat
Hrecn:x ^ n <= Rabs x ^ n
Hle:x >= 0
x * x ^ n <= Rabs x * Rabs x ^ n
  apply Rle_trans with (Rabs (x * x ^ n)).x:R
n:nat
Hrecn:x ^ n <= Rabs x ^ n
Hlt:x < 0
x * x ^ n <= Rabs (x * x ^ n)
x:R
n:nat
Hrecn:x ^ n <= Rabs x ^ n
Hlt:x < 0
Rabs (x * x ^ n) <= Rabs x * Rabs x ^ n
x:R
n:nat
Hrecn:x ^ n <= Rabs x ^ n
Hle:x >= 0
x * x ^ n <= Rabs x * Rabs x ^ n
  apply RRle_abs.x:R
n:nat
Hrecn:x ^ n <= Rabs x ^ n
Hlt:x < 0
Rabs (x * x ^ n) <= Rabs x * Rabs x ^ n
x:R
n:nat
Hrecn:x ^ n <= Rabs x ^ n
Hle:x >= 0
x * x ^ n <= Rabs x * Rabs x ^ n
  rewrite Rabs_mult.x:R
n:nat
Hrecn:x ^ n <= Rabs x ^ n
Hlt:x < 0
Rabs x * Rabs (x ^ n) <= Rabs x * Rabs x ^ n
x:R
n:nat
Hrecn:x ^ n <= Rabs x ^ n
Hle:x >= 0
x * x ^ n <= Rabs x * Rabs x ^ n
  apply Rmult_le_compat_l.x:R
n:nat
Hrecn:x ^ n <= Rabs x ^ n
Hlt:x < 0
0 <= Rabs x
x:R
n:nat
Hrecn:x ^ n <= Rabs x ^ n
Hlt:x < 0
Rabs (x ^ n) <= Rabs x ^ n
x:R
n:nat
Hrecn:x ^ n <= Rabs x ^ n
Hle:x >= 0
x * x ^ n <= Rabs x * Rabs x ^ n
  apply Rabs_pos.x:R
n:nat
Hrecn:x ^ n <= Rabs x ^ n
Hlt:x < 0
Rabs (x ^ n) <= Rabs x ^ n
x:R
n:nat
Hrecn:x ^ n <= Rabs x ^ n
Hle:x >= 0
x * x ^ n <= Rabs x * Rabs x ^ n
  right; symmetry; apply RPow_abs.x:R
n:nat
Hrecn:x ^ n <= Rabs x ^ n
Hle:x >= 0
x * x ^ n <= Rabs x * Rabs x ^ n
  pattern (Rabs x) at 1; rewrite (Rabs_right x Hle);
    apply Rmult_le_compat_l.x:R
n:nat
Hrecn:x ^ n <= Rabs x ^ n
Hle:x >= 0
0 <= x
x:R
n:nat
Hrecn:x ^ n <= Rabs x ^ n
Hle:x >= 0
x ^ n <= Rabs x ^ n
  apply Rge_le; exact Hle.x:R
n:nat
Hrecn:x ^ n <= Rabs x ^ n
Hle:x >= 0
x ^ n <= Rabs x ^ n
  apply Hrecn.
Qed.

Lemma pow_maj_Rabs : forall (x y:R) (n:nat), Rabs y <= x -> y ^ n <= x ^ n.forall (x y : R) (n : nat),
Rabs y <= x -> y ^ n <= x ^ n
Proof.forall (x y : R) (n : nat),
Rabs y <= x -> y ^ n <= x ^ n
  intros; cut (0 <= x).x, y:R
n:nat
H:Rabs y <= x
0 <= x -> y ^ n <= x ^ n
x, y:R
n:nat
H:Rabs y <= x
0 <= x
  intro; apply Rle_trans with (Rabs y ^ n).x, y:R
n:nat
H:Rabs y <= x
H0:0 <= x
y ^ n <= Rabs y ^ n
x, y:R
n:nat
H:Rabs y <= x
H0:0 <= x
Rabs y ^ n <= x ^ n
x, y:R
n:nat
H:Rabs y <= x
0 <= x
  apply pow_Rabs.x, y:R
n:nat
H:Rabs y <= x
H0:0 <= x
Rabs y ^ n <= x ^ n
x, y:R
n:nat
H:Rabs y <= x
0 <= x
  induction  n as [| n Hrecn].x, y:R
H:Rabs y <= x
H0:0 <= x
Rabs y ^ 0 <= x ^ 0
x, y:R
n:nat
H:Rabs y <= x
H0:0 <= x
Hrecn:Rabs y ^ n <= x ^ n
Rabs y ^ S n <= x ^ S n
x, y:R
n:nat
H:Rabs y <= x
0 <= x
  right; reflexivity.x, y:R
n:nat
H:Rabs y <= x
H0:0 <= x
Hrecn:Rabs y ^ n <= x ^ n
Rabs y ^ S n <= x ^ S n
x, y:R
n:nat
H:Rabs y <= x
0 <= x
  simpl; apply Rle_trans with (x * Rabs y ^ n).x, y:R
n:nat
H:Rabs y <= x
H0:0 <= x
Hrecn:Rabs y ^ n <= x ^ n
Rabs y * Rabs y ^ n <= x * Rabs y ^ n
x, y:R
n:nat
H:Rabs y <= x
H0:0 <= x
Hrecn:Rabs y ^ n <= x ^ n
x * Rabs y ^ n <= x * x ^ n
x, y:R
n:nat
H:Rabs y <= x
0 <= x
  do 2 rewrite <- (Rmult_comm (Rabs y ^ n)).x, y:R
n:nat
H:Rabs y <= x
H0:0 <= x
Hrecn:Rabs y ^ n <= x ^ n
Rabs y ^ n * Rabs y <= Rabs y ^ n * x
x, y:R
n:nat
H:Rabs y <= x
H0:0 <= x
Hrecn:Rabs y ^ n <= x ^ n
x * Rabs y ^ n <= x * x ^ n
x, y:R
n:nat
H:Rabs y <= x
0 <= x
  apply Rmult_le_compat_l.x, y:R
n:nat
H:Rabs y <= x
H0:0 <= x
Hrecn:Rabs y ^ n <= x ^ n
0 <= Rabs y ^ n
x, y:R
n:nat
H:Rabs y <= x
H0:0 <= x
Hrecn:Rabs y ^ n <= x ^ n
Rabs y <= x
x, y:R
n:nat
H:Rabs y <= x
H0:0 <= x
Hrecn:Rabs y ^ n <= x ^ n
x * Rabs y ^ n <= x * x ^ n
x, y:R
n:nat
H:Rabs y <= x
0 <= x
  apply pow_le; apply Rabs_pos.x, y:R
n:nat
H:Rabs y <= x
H0:0 <= x
Hrecn:Rabs y ^ n <= x ^ n
Rabs y <= x
x, y:R
n:nat
H:Rabs y <= x
H0:0 <= x
Hrecn:Rabs y ^ n <= x ^ n
x * Rabs y ^ n <= x * x ^ n
x, y:R
n:nat
H:Rabs y <= x
0 <= x
  assumption.x, y:R
n:nat
H:Rabs y <= x
H0:0 <= x
Hrecn:Rabs y ^ n <= x ^ n
x * Rabs y ^ n <= x * x ^ n
x, y:R
n:nat
H:Rabs y <= x
0 <= x
  apply Rmult_le_compat_l.x, y:R
n:nat
H:Rabs y <= x
H0:0 <= x
Hrecn:Rabs y ^ n <= x ^ n
0 <= x
x, y:R
n:nat
H:Rabs y <= x
H0:0 <= x
Hrecn:Rabs y ^ n <= x ^ n
Rabs y ^ n <= x ^ n
x, y:R
n:nat
H:Rabs y <= x
0 <= x
  apply H0.x, y:R
n:nat
H:Rabs y <= x
H0:0 <= x
Hrecn:Rabs y ^ n <= x ^ n
Rabs y ^ n <= x ^ n
x, y:R
n:nat
H:Rabs y <= x
0 <= x
  apply Hrecn.x, y:R
n:nat
H:Rabs y <= x
0 <= x
  apply Rle_trans with (Rabs y); [ apply Rabs_pos | exact H ].
Qed.

Lemma Rsqr_pow2 : forall x, Rsqr x = x ^ 2.forall x : R, x² = x ^ 2
Proof.forall x : R, x² = x ^ 2
intros; unfold Rsqr; simpl; rewrite Rmult_1_r; reflexivity.
Qed.


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

PowerRZ

(*******************************)
(*i Due to L.Thery i*)

Section PowerRZ.

Coercion Z_of_nat : nat >-> Z.

(* the following section should probably be somewhere else, but not sure where *)
Section Z_compl.

Local Open Scope Z_scope.

(* Provides a way to reason directly on Z in terms of nats instead of positive *)
Inductive Z_spec (x : Z) : Z -> Type :=
| ZintNull : x = 0 -> Z_spec x 0
| ZintPos (n : nat) : x = n -> Z_spec x n
| ZintNeg (n : nat) : x = - n -> Z_spec x (- n).

Lemma intP (x : Z) : Z_spec x x.x:Z
Z_spec x x
Proof.x:Z
Z_spec x x
  destruct x as [|p|p].Z_spec 0 0
p:positive
Z_spec (Z.pos p) (Z.pos p)
p:positive
Z_spec (Z.neg p) (Z.neg p)
  -Z_spec 0 0 now apply ZintNull.
  -p:positive
Z_spec (Z.pos p) (Z.pos p) rewrite <-positive_nat_Z at 2.p:positive
Z_spec (Z.pos p) (Pos.to_nat p)
    apply ZintPos.p:positive
Z.pos p = Pos.to_nat p
    now rewrite positive_nat_Z.
  -p:positive
Z_spec (Z.neg p) (Z.neg p) rewrite <-Pos2Z.opp_pos.p:positive
Z_spec (- Z.pos p) (- Z.pos p)
    rewrite <-positive_nat_Z at 2.p:positive
Z_spec (- Z.pos p) (- Pos.to_nat p)
    apply ZintNeg.p:positive
- Z.pos p = - Pos.to_nat p
    now rewrite positive_nat_Z.
Qed.

End Z_compl.

Definition powerRZ (x:R) (n:Z) :=
  match n with
    | Z0 => 1
    | Zpos p => x ^ Pos.to_nat p
    | Zneg p => / x ^ Pos.to_nat p
  end.

Local Infix "^Z" := powerRZ (at level 30, right associativity) : R_scope.

Lemma Zpower_NR0 :
  forall (x:Z) (n:nat), (0 <= x)%Z -> (0 <= Zpower_nat x n)%Z.forall (x : Z) (n : nat),
(0 <= x)%Z -> (0 <= Zpower_nat x n)%Z
Proof.forall (x : Z) (n : nat),
(0 <= x)%Z -> (0 <= Zpower_nat x n)%Z
  induction n; unfold Zpower_nat; simpl; auto with zarith.
Qed.

Lemma powerRZ_O : forall x:R, x ^Z 0 = 1.forall x : R, x ^Z 0 = 1
Proof.forall x : R, x ^Z 0 = 1
  reflexivity.
Qed.

Lemma powerRZ_1 : forall x:R, x ^Z Z.succ 0 = x.forall x : R, x ^Z Z.succ 0 = x
Proof.forall x : R, x ^Z Z.succ 0 = x
  simpl; auto with real.
Qed.

Lemma powerRZ_NOR : forall (x:R) (z:Z), x <> 0 -> x ^Z z <> 0.forall (x : R) (z : Z), x <> 0 -> x ^Z z <> 0
Proof.forall (x : R) (z : Z), x <> 0 -> x ^Z z <> 0
  destruct z; simpl; auto with real.
Qed.

Lemma powerRZ_pos_sub (x:R) (n m:positive) : x <> 0 ->
   x ^Z (Z.pos_sub n m) = x ^ Pos.to_nat n * / x ^ Pos.to_nat m.x:R
n, m:positive
x <> 0 ->
x ^Z Z.pos_sub n m =
x ^ Pos.to_nat n * / x ^ Pos.to_nat m
Proof.x:R
n, m:positive
x <> 0 ->
x ^Z Z.pos_sub n m =
x ^ Pos.to_nat n * / x ^ Pos.to_nat m
 intro Hx.x:R
n, m:positive
Hx:x <> 0
x ^Z Z.pos_sub n m =
x ^ Pos.to_nat n * / x ^ Pos.to_nat m
 rewrite Z.pos_sub_spec.x:R
n, m:positive
Hx:x <> 0
x
^Z match (n ?= m)%positive with
   | Eq => 0
   | Lt => Z.neg (m - n)
   | Gt => Z.pos (n - m)
   end = x ^ Pos.to_nat n * / x ^ Pos.to_nat m
 case Pos.compare_spec; intro H; simpl.x:R
n, m:positive
Hx:x <> 0
H:n = m
1 = x ^ Pos.to_nat n * / x ^ Pos.to_nat m
x:R
n, m:positive
Hx:x <> 0
H:(n < m)%positive
/ x ^ Pos.to_nat (m - n) =
x ^ Pos.to_nat n * / x ^ Pos.to_nat m
x:R
n, m:positive
Hx:x <> 0
H:(m < n)%positive
x ^ Pos.to_nat (n - m) =
x ^ Pos.to_nat n * / x ^ Pos.to_nat m
 -x:R
n, m:positive
Hx:x <> 0
H:n = m
1 = x ^ Pos.to_nat n * / x ^ Pos.to_nat m subst; auto with real.
 -x:R
n, m:positive
Hx:x <> 0
H:(n < m)%positive
/ x ^ Pos.to_nat (m - n) =
x ^ Pos.to_nat n * / x ^ Pos.to_nat m rewrite Pos2Nat.inj_sub by trivial.x:R
n, m:positive
Hx:x <> 0
H:(n < m)%positive
/ x ^ (Pos.to_nat m - Pos.to_nat n) =
x ^ Pos.to_nat n * / x ^ Pos.to_nat m
   rewrite Pos2Nat.inj_lt in H.x:R
n, m:positive
Hx:x <> 0
H:(Pos.to_nat n < Pos.to_nat m)%nat
/ x ^ (Pos.to_nat m - Pos.to_nat n) =
x ^ Pos.to_nat n * / x ^ Pos.to_nat m
   rewrite (pow_RN_plus x _ (Pos.to_nat n)) by auto with real.x:R
n, m:positive
Hx:x <> 0
H:(Pos.to_nat n < Pos.to_nat m)%nat
/
(x ^ (Pos.to_nat m - Pos.to_nat n + Pos.to_nat n) *
 / x ^ Pos.to_nat n) =
x ^ Pos.to_nat n * / x ^ Pos.to_nat m
   rewrite plus_comm, le_plus_minus_r by auto with real.x:R
n, m:positive
Hx:x <> 0
H:(Pos.to_nat n < Pos.to_nat m)%nat
/ (x ^ Pos.to_nat m * / x ^ Pos.to_nat n) =
x ^ Pos.to_nat n * / x ^ Pos.to_nat m
   rewrite Rinv_mult_distr, Rinv_involutive; auto with real.
 -x:R
n, m:positive
Hx:x <> 0
H:(m < n)%positive
x ^ Pos.to_nat (n - m) =
x ^ Pos.to_nat n * / x ^ Pos.to_nat m rewrite Pos2Nat.inj_sub by trivial.x:R
n, m:positive
Hx:x <> 0
H:(m < n)%positive
x ^ (Pos.to_nat n - Pos.to_nat m) =
x ^ Pos.to_nat n * / x ^ Pos.to_nat m
   rewrite Pos2Nat.inj_lt in H.x:R
n, m:positive
Hx:x <> 0
H:(Pos.to_nat m < Pos.to_nat n)%nat
x ^ (Pos.to_nat n - Pos.to_nat m) =
x ^ Pos.to_nat n * / x ^ Pos.to_nat m
   rewrite (pow_RN_plus x _ (Pos.to_nat m)) by auto with real.x:R
n, m:positive
Hx:x <> 0
H:(Pos.to_nat m < Pos.to_nat n)%nat
x ^ (Pos.to_nat n - Pos.to_nat m + Pos.to_nat m) *
/ x ^ Pos.to_nat m =
x ^ Pos.to_nat n * / x ^ Pos.to_nat m
   rewrite plus_comm, le_plus_minus_r by auto with real.x:R
n, m:positive
Hx:x <> 0
H:(Pos.to_nat m < Pos.to_nat n)%nat
x ^ Pos.to_nat n * / x ^ Pos.to_nat m =
x ^ Pos.to_nat n * / x ^ Pos.to_nat m
   reflexivity.
Qed.

Lemma powerRZ_add :
  forall (x:R) (n m:Z), x <> 0 -> x ^Z (n + m) = x ^Z n * x ^Z m.forall (x : R) (n m : Z),
x <> 0 -> x ^Z (n + m) = x ^Z n * x ^Z m
Proof.forall (x : R) (n m : Z),
x <> 0 -> x ^Z (n + m) = x ^Z n * x ^Z m
  intros x [|n|n] [|m|m]; simpl; intros; auto with real.x:R
n, m:positive
H:x <> 0
x ^ Pos.to_nat (n + m) =
x ^ Pos.to_nat n * x ^ Pos.to_nat m
x:R
n, m:positive
H:x <> 0
x ^Z Z.pos_sub n m =
x ^ Pos.to_nat n * / x ^ Pos.to_nat m
x:R
n, m:positive
H:x <> 0
x ^Z Z.pos_sub m n =
/ x ^ Pos.to_nat n * x ^ Pos.to_nat m
x:R
n, m:positive
H:x <> 0
/ x ^ Pos.to_nat (n + m) =
/ x ^ Pos.to_nat n * / x ^ Pos.to_nat m
  - (* + + *)x:R
n, m:positive
H:x <> 0
x ^ Pos.to_nat (n + m) =
x ^ Pos.to_nat n * x ^ Pos.to_nat m
    rewrite Pos2Nat.inj_add; auto with real.
  - (* + - *)x:R
n, m:positive
H:x <> 0
x ^Z Z.pos_sub n m =
x ^ Pos.to_nat n * / x ^ Pos.to_nat m
    now apply powerRZ_pos_sub.
  - (* - + *)x:R
n, m:positive
H:x <> 0
x ^Z Z.pos_sub m n =
/ x ^ Pos.to_nat n * x ^ Pos.to_nat m
    rewrite Rmult_comm.x:R
n, m:positive
H:x <> 0
x ^Z Z.pos_sub m n =
x ^ Pos.to_nat m * / x ^ Pos.to_nat n now apply powerRZ_pos_sub.
  - (* - - *)x:R
n, m:positive
H:x <> 0
/ x ^ Pos.to_nat (n + m) =
/ x ^ Pos.to_nat n * / x ^ Pos.to_nat m
    rewrite Pos2Nat.inj_add; auto with real.x:R
n, m:positive
H:x <> 0
/ x ^ (Pos.to_nat n + Pos.to_nat m) =
/ x ^ Pos.to_nat n * / x ^ Pos.to_nat m
    rewrite pow_add; auto with real.x:R
n, m:positive
H:x <> 0
/ (x ^ Pos.to_nat n * x ^ Pos.to_nat m) =
/ x ^ Pos.to_nat n * / x ^ Pos.to_nat m
    apply Rinv_mult_distr; apply pow_nonzero; auto.
Qed.
Hint Resolve powerRZ_O powerRZ_1 powerRZ_NOR powerRZ_add: real.

Lemma Zpower_nat_powerRZ :
  forall n m:nat, IZR (Zpower_nat (Z.of_nat n) m) = INR n ^Z Z.of_nat m.forall n m : nat, IZR (Zpower_nat n m) = INR n ^Z m
Proof.forall n m : nat, IZR (Zpower_nat n m) = INR n ^Z m
  intros n m; elim m; simpl; auto with real.n, m:nat
forall n0 : nat,
IZR (Zpower_nat n n0) = INR n ^Z n0 ->
IZR (n * Zpower_nat n n0) =
INR n ^ Pos.to_nat (Pos.of_succ_nat n0)
  intros m1 H'; rewrite SuccNat2Pos.id_succ; simpl.n, m, m1:nat
H':IZR (Zpower_nat n m1) = INR n ^Z m1
IZR (n * Zpower_nat n m1) = INR n * INR n ^ m1
  replace (Zpower_nat (Z.of_nat n) (S m1)) with
  (Z.of_nat n * Zpower_nat (Z.of_nat n) m1)%Z.n, m, m1:nat
H':IZR (Zpower_nat n m1) = INR n ^Z m1
IZR (n * Zpower_nat n m1) = INR n * INR n ^ m1
n, m, m1:nat
H':IZR (Zpower_nat n m1) = INR n ^Z m1
(n * Zpower_nat n m1)%Z = Zpower_nat n (S m1)
  rewrite mult_IZR; auto with real.n, m, m1:nat
H':IZR (Zpower_nat n m1) = INR n ^Z m1
IZR n * IZR (Zpower_nat n m1) = INR n * INR n ^ m1
n, m, m1:nat
H':IZR (Zpower_nat n m1) = INR n ^Z m1
(n * Zpower_nat n m1)%Z = Zpower_nat n (S m1)
  repeat rewrite <- INR_IZR_INZ; simpl.n, m, m1:nat
H':IZR (Zpower_nat n m1) = INR n ^Z m1
INR n * IZR (Zpower_nat n m1) = INR n * INR n ^ m1
n, m, m1:nat
H':IZR (Zpower_nat n m1) = INR n ^Z m1
(n * Zpower_nat n m1)%Z = Zpower_nat n (S m1)
  rewrite H'; simpl.n, m, m1:nat
H':IZR (Zpower_nat n m1) = INR n ^Z m1
INR n * INR n ^Z m1 = INR n * INR n ^ m1
n, m, m1:nat
H':IZR (Zpower_nat n m1) = INR n ^Z m1
(n * Zpower_nat n m1)%Z = Zpower_nat n (S m1)
  case m1; simpl; auto with real.n, m, m1:nat
H':IZR (Zpower_nat n m1) = INR n ^Z m1
forall n0 : nat,
INR n * INR n ^ Pos.to_nat (Pos.of_succ_nat n0) =
INR n * (INR n * INR n ^ n0)
n, m, m1:nat
H':IZR (Zpower_nat n m1) = INR n ^Z m1
(n * Zpower_nat n m1)%Z = Zpower_nat n (S m1)
  intros m2; rewrite SuccNat2Pos.id_succ; auto.n, m, m1:nat
H':IZR (Zpower_nat n m1) = INR n ^Z m1
(n * Zpower_nat n m1)%Z = Zpower_nat n (S m1)
  unfold Zpower_nat; auto.
Qed.

Lemma Zpower_pos_powerRZ :
  forall n m, IZR (Z.pow_pos n m) = IZR n ^Z Zpos m.forall (n : Z) (m : positive),
IZR (Z.pow_pos n m) = IZR n ^Z Z.pos m
Proof.forall (n : Z) (m : positive),
IZR (Z.pow_pos n m) = IZR n ^Z Z.pos m
  intros.n:Z
m:positive
IZR (Z.pow_pos n m) = IZR n ^Z Z.pos m
  rewrite Zpower_pos_nat; simpl.n:Z
m:positive
IZR (Zpower_nat n (Pos.to_nat m)) =
IZR n ^ Pos.to_nat m
  induction (Pos.to_nat m).n:Z
m:positive
IZR (Zpower_nat n 0) = IZR n ^ 0
n:Z
m:positive
n0:nat
IHn0:IZR (Zpower_nat n n0) = IZR n ^ n0
IZR (Zpower_nat n (S n0)) = IZR n ^ S n0
  easy.n:Z
m:positive
n0:nat
IHn0:IZR (Zpower_nat n n0) = IZR n ^ n0
IZR (Zpower_nat n (S n0)) = IZR n ^ S n0
  unfold Zpower_nat; simpl.n:Z
m:positive
n0:nat
IHn0:IZR (Zpower_nat n n0) = IZR n ^ n0
IZR
  (n *
   nat_rect (fun _ : nat => Z) 1%Z
     (fun _ : nat => Z.mul n) n0) = IZR n * IZR n ^ n0
  rewrite mult_IZR.n:Z
m:positive
n0:nat
IHn0:IZR (Zpower_nat n n0) = IZR n ^ n0
IZR n *
IZR
  (nat_rect (fun _ : nat => Z) 1%Z
     (fun _ : nat => Z.mul n) n0) = IZR n * IZR n ^ n0
  now rewrite <- IHn0.
Qed.

Lemma powerRZ_lt : forall (x:R) (z:Z), 0 < x -> 0 < x ^Z z.forall (x : R) (z : Z), 0 < x -> 0 < x ^Z z
Proof.forall (x : R) (z : Z), 0 < x -> 0 < x ^Z z
  intros x z; case z; simpl; auto with real.
Qed.
Hint Resolve powerRZ_lt: real.

Lemma powerRZ_le : forall (x:R) (z:Z), 0 < x -> 0 <= x ^Z z.forall (x : R) (z : Z), 0 < x -> 0 <= x ^Z z
Proof.forall (x : R) (z : Z), 0 < x -> 0 <= x ^Z z
  intros x z H'; apply Rlt_le; auto with real.
Qed.
Hint Resolve powerRZ_le: real.

Lemma Zpower_nat_powerRZ_absolu :
  forall n m:Z, (0 <= m)%Z -> IZR (Zpower_nat n (Z.abs_nat m)) = IZR n ^Z m.forall n m : Z,
(0 <= m)%Z ->
IZR (Zpower_nat n (Z.abs_nat m)) = IZR n ^Z m
Proof.forall n m : Z,
(0 <= m)%Z ->
IZR (Zpower_nat n (Z.abs_nat m)) = IZR n ^Z m
  intros n m; case m; simpl; auto with zarith.n, m:Z
forall p : positive,
(0 <= Z.pos p)%Z ->
IZR (Zpower_nat n (Pos.to_nat p)) =
IZR n ^ Pos.to_nat p
n, m:Z
forall p : positive,
(0 <= Z.neg p)%Z ->
IZR (Zpower_nat n (Pos.to_nat p)) =
/ IZR n ^ Pos.to_nat p
  intros p H'; elim (Pos.to_nat p); simpl; auto with zarith.n, m:Z
p:positive
H':(0 <= Z.pos p)%Z
forall n0 : nat,
IZR (Zpower_nat n n0) = IZR n ^ n0 ->
IZR (n * Zpower_nat n n0) = IZR n * IZR n ^ n0
n, m:Z
forall p : positive,
(0 <= Z.neg p)%Z ->
IZR (Zpower_nat n (Pos.to_nat p)) =
/ IZR n ^ Pos.to_nat p
  intros n0 H'0; rewrite <- H'0; simpl; auto with zarith.n, m:Z
p:positive
H':(0 <= Z.pos p)%Z
n0:nat
H'0:IZR (Zpower_nat n n0) = IZR n ^ n0
IZR (n * Zpower_nat n n0) =
IZR n * IZR (Zpower_nat n n0)
n, m:Z
forall p : positive,
(0 <= Z.neg p)%Z ->
IZR (Zpower_nat n (Pos.to_nat p)) =
/ IZR n ^ Pos.to_nat p
  rewrite <- mult_IZR; auto.n, m:Z
forall p : positive,
(0 <= Z.neg p)%Z ->
IZR (Zpower_nat n (Pos.to_nat p)) =
/ IZR n ^ Pos.to_nat p
  intros p H'; absurd (0 <= Zneg p)%Z; auto with zarith.
Qed.

Lemma powerRZ_R1 : forall n:Z, 1 ^Z n = 1.forall n : Z, 1 ^Z n = 1
Proof.forall n : Z, 1 ^Z n = 1
  intros n; case n; simpl; auto.n:Z
forall p : positive, 1 ^ Pos.to_nat p = 1
n:Z
forall p : positive, / 1 ^ Pos.to_nat p = 1
  intros p; elim (Pos.to_nat p); simpl; auto; intros n0 H'; rewrite H';
    ring.n:Z
forall p : positive, / 1 ^ Pos.to_nat p = 1
  intros p; elim (Pos.to_nat p); simpl.n:Z
p:positive
/ 1 = 1
n:Z
p:positive
forall n0 : nat, / 1 ^ n0 = 1 -> / (1 * 1 ^ n0) = 1
  exact Rinv_1.n:Z
p:positive
forall n0 : nat, / 1 ^ n0 = 1 -> / (1 * 1 ^ n0) = 1
  intros n1 H'; rewrite Rinv_mult_distr; try rewrite Rinv_1; try rewrite H';
    auto with real.
Qed.

Local Open Scope Z_scope.

Lemma pow_powerRZ (r : R) (n : nat) :
  (r ^ n)%R = powerRZ r (Z_of_nat n).r:R
n:nat
(r ^ n)%R = r ^Z n
Proof.r:R
n:nat
(r ^ n)%R = r ^Z n
  induction n; [easy|simpl].r:R
n:nat
IHn:(r ^ n)%R = r ^Z n
(r * r ^ n)%R = (r ^ Pos.to_nat (Pos.of_succ_nat n))%R
  now rewrite SuccNat2Pos.id_succ.
Qed.

Lemma powerRZ_ind (P : Z -> R -> R -> Prop) :
  (forall x, P 0 x 1%R) ->
  (forall x n, P (Z.of_nat n) x (x ^ n)%R) ->
  (forall x n, P ((-(Z.of_nat n))%Z) x (Rinv (x ^ n))) ->
  forall x (m : Z), P m x (powerRZ x m)%R.P:Z -> R -> R -> Prop
(forall x : R, P 0 x 1%R) ->
(forall (x : R) (n : nat), P n x (x ^ n)%R) ->
(forall (x : R) (n : nat), P (- n) x (/ x ^ n)) ->
forall (x : R) (m : Z), P m x (x ^Z m)
Proof.P:Z -> R -> R -> Prop
(forall x : R, P 0 x 1%R) ->
(forall (x : R) (n : nat), P n x (x ^ n)%R) ->
(forall (x : R) (n : nat), P (- n) x (/ x ^ n)) ->
forall (x : R) (m : Z), P m x (x ^Z m)
  intros ? ? ? x m.P:Z -> R -> R -> Prop
H:forall x0 : R, P 0 x0 1%R
H0:forall (x0 : R) (n : nat), P n x0 (x0 ^ n)%R
H1:forall (x0 : R) (n : nat), P (- n) x0 (/ x0 ^ n)
x:R
m:Z
P m x (x ^Z m)
  destruct (intP m) as [Hm|n Hm|n Hm].P:Z -> R -> R -> Prop
H:forall x0 : R, P 0 x0 1%R
H0:forall (x0 : R) (n : nat), P n x0 (x0 ^ n)%R
H1:forall (x0 : R) (n : nat), P (- n) x0 (/ x0 ^ n)
x:R
m:Z
Hm:m = 0
P 0 x (x ^Z 0)
P:Z -> R -> R -> Prop
H:forall x0 : R, P 0 x0 1%R
H0:forall (x0 : R) (n0 : nat), P n0 x0 (x0 ^ n0)%R
H1:forall (x0 : R) (n0 : nat),
P (- n0) x0 (/ x0 ^ n0)
x:R
m:Z
n:nat
Hm:m = n
P n x (x ^Z n)
P:Z -> R -> R -> Prop
H:forall x0 : R, P 0 x0 1%R
H0:forall (x0 : R) (n0 : nat), P n0 x0 (x0 ^ n0)%R
H1:forall (x0 : R) (n0 : nat),
P (- n0) x0 (/ x0 ^ n0)
x:R
m:Z
n:nat
Hm:m = - n
P (- n) x (x ^Z (- n))
  -P:Z -> R -> R -> Prop
H:forall x0 : R, P 0 x0 1%R
H0:forall (x0 : R) (n : nat), P n x0 (x0 ^ n)%R
H1:forall (x0 : R) (n : nat), P (- n) x0 (/ x0 ^ n)
x:R
m:Z
Hm:m = 0
P 0 x (x ^Z 0) easy.
  -P:Z -> R -> R -> Prop
H:forall x0 : R, P 0 x0 1%R
H0:forall (x0 : R) (n0 : nat), P n0 x0 (x0 ^ n0)%R
H1:forall (x0 : R) (n0 : nat),
P (- n0) x0 (/ x0 ^ n0)
x:R
m:Z
n:nat
Hm:m = n
P n x (x ^Z n) now rewrite <- pow_powerRZ.
  -P:Z -> R -> R -> Prop
H:forall x0 : R, P 0 x0 1%R
H0:forall (x0 : R) (n0 : nat), P n0 x0 (x0 ^ n0)%R
H1:forall (x0 : R) (n0 : nat),
P (- n0) x0 (/ x0 ^ n0)
x:R
m:Z
n:nat
Hm:m = - n
P (- n) x (x ^Z (- n)) unfold powerRZ.P:Z -> R -> R -> Prop
H:forall x0 : R, P 0 x0 1%R
H0:forall (x0 : R) (n0 : nat), P n0 x0 (x0 ^ n0)%R
H1:forall (x0 : R) (n0 : nat),
P (- n0) x0 (/ x0 ^ n0)
x:R
m:Z
n:nat
Hm:m = - n
P (- n) x
  match - n with
  | 0 => 1%R
  | Z.pos p => (x ^ Pos.to_nat p)%R
  | Z.neg p => / x ^ Pos.to_nat p
  end
    destruct n as [|n]; [ easy |].P:Z -> R -> R -> Prop
H:forall x0 : R, P 0 x0 1%R
H0:forall (x0 : R) (n0 : nat), P n0 x0 (x0 ^ n0)%R
H1:forall (x0 : R) (n0 : nat),
P (- n0) x0 (/ x0 ^ n0)
x:R
m:Z
n:nat
Hm:m = - S n
P (- S n) x
  match - S n with
  | 0 => 1%R
  | Z.pos p => (x ^ Pos.to_nat p)%R
  | Z.neg p => / x ^ Pos.to_nat p
  end
    rewrite Nat2Z.inj_succ, <- Zpos_P_of_succ_nat, Pos2Z.opp_pos.P:Z -> R -> R -> Prop
H:forall x0 : R, P 0 x0 1%R
H0:forall (x0 : R) (n0 : nat), P n0 x0 (x0 ^ n0)%R
H1:forall (x0 : R) (n0 : nat),
P (- n0) x0 (/ x0 ^ n0)
x:R
m:Z
n:nat
Hm:m = - S n
P (Z.neg (Pos.of_succ_nat n)) x
  (/ x ^ Pos.to_nat (Pos.of_succ_nat n))
    now rewrite <- Pos2Z.opp_pos, <- positive_nat_Z.
Qed.

Lemma powerRZ_inv x alpha : (x <> 0)%R -> powerRZ (/ x) alpha = Rinv (powerRZ x alpha).x:R
alpha:Z
x <> 0%R -> (/ x) ^Z alpha = / x ^Z alpha
Proof.x:R
alpha:Z
x <> 0%R -> (/ x) ^Z alpha = / x ^Z alpha
  intros; destruct (intP alpha).x:R
alpha:Z
H:x <> 0%R
e:alpha = 0
(/ x) ^Z 0 = / x ^Z 0
x:R
alpha:Z
H:x <> 0%R
n:nat
e:alpha = n
(/ x) ^Z n = / x ^Z n
x:R
alpha:Z
H:x <> 0%R
n:nat
e:alpha = - n
(/ x) ^Z (- n) = / x ^Z (- n)
  -x:R
alpha:Z
H:x <> 0%R
e:alpha = 0
(/ x) ^Z 0 = / x ^Z 0 now simpl; rewrite Rinv_1.
  -x:R
alpha:Z
H:x <> 0%R
n:nat
e:alpha = n
(/ x) ^Z n = / x ^Z n now rewrite <-!pow_powerRZ, ?Rinv_pow, ?pow_powerRZ.
  -x:R
alpha:Z
H:x <> 0%R
n:nat
e:alpha = - n
(/ x) ^Z (- n) = / x ^Z (- n) unfold powerRZ.x:R
alpha:Z
H:x <> 0%R
n:nat
e:alpha = - n
match - n with
| 0 => 1%R
| Z.pos p => ((/ x) ^ Pos.to_nat p)%R
| Z.neg p => / (/ x) ^ Pos.to_nat p
end =
/
match - n with
| 0%Z => 1
| Z.pos p => x ^ Pos.to_nat p
| Z.neg p => / x ^ Pos.to_nat p
end
    destruct (- n).x:R
alpha:Z
H:x <> 0%R
n:nat
e:alpha = 0
1%R = / 1
x:R
alpha:Z
H:x <> 0%R
n:nat
p:positive
e:alpha = Z.pos p
((/ x) ^ Pos.to_nat p)%R = / x ^ Pos.to_nat p
x:R
alpha:Z
H:x <> 0%R
n:nat
p:positive
e:alpha = Z.neg p
/ (/ x) ^ Pos.to_nat p = / / x ^ Pos.to_nat p
    +x:R
alpha:Z
H:x <> 0%R
n:nat
e:alpha = 0
1%R = / 1 now rewrite Rinv_1.
    +x:R
alpha:Z
H:x <> 0%R
n:nat
p:positive
e:alpha = Z.pos p
((/ x) ^ Pos.to_nat p)%R = / x ^ Pos.to_nat p now rewrite Rinv_pow.
    +x:R
alpha:Z
H:x <> 0%R
n:nat
p:positive
e:alpha = Z.neg p
/ (/ x) ^ Pos.to_nat p = / / x ^ Pos.to_nat p now rewrite <-Rinv_pow.
Qed.

Lemma powerRZ_neg x : forall alpha, x <> R0 -> powerRZ x (- alpha) = powerRZ (/ x) alpha.x:R
forall alpha : Z,
x <> R0 -> x ^Z (- alpha) = (/ x) ^Z alpha
Proof.x:R
forall alpha : Z,
x <> R0 -> x ^Z (- alpha) = (/ x) ^Z alpha
  intros [|n|n] H ; simpl.x:R
H:x <> R0
1%R = 1%R
x:R
n:positive
H:x <> R0
/ x ^ Pos.to_nat n = ((/ x) ^ Pos.to_nat n)%R
x:R
n:positive
H:x <> R0
(x ^ Pos.to_nat n)%R = / (/ x) ^ Pos.to_nat n
  -x:R
H:x <> R0
1%R = 1%R easy.
  -x:R
n:positive
H:x <> R0
/ x ^ Pos.to_nat n = ((/ x) ^ Pos.to_nat n)%R now rewrite Rinv_pow.
  -x:R
n:positive
H:x <> R0
(x ^ Pos.to_nat n)%R = / (/ x) ^ Pos.to_nat n rewrite Rinv_pow by now apply Rinv_neq_0_compat.x:R
n:positive
H:x <> R0
(x ^ Pos.to_nat n)%R = ((/ / x) ^ Pos.to_nat n)%R
    now rewrite Rinv_involutive.
Qed.

Lemma powerRZ_mult_distr :
  forall m x y, ((0 <= m)%Z \/ (x * y <> 0)%R) ->
           (powerRZ (x*y) m = powerRZ x m * powerRZ y m)%R.forall (m : Z) (x y : R),
0 <= m \/ (x * y)%R <> 0%R ->
(x * y) ^Z m = (x ^Z m * y ^Z m)%R
Proof.forall (m : Z) (x y : R),
0 <= m \/ (x * y)%R <> 0%R ->
(x * y) ^Z m = (x ^Z m * y ^Z m)%R
  intros m x0 y0 Hmxy.m:Z
x0, y0:R
Hmxy:0 <= m \/ (x0 * y0)%R <> 0%R
(x0 * y0) ^Z m = (x0 ^Z m * y0 ^Z m)%R
  destruct (intP m) as [ | | n Hm ].m:Z
x0, y0:R
Hmxy:0 <= m \/ (x0 * y0)%R <> 0%R
e:m = 0
(x0 * y0) ^Z 0 = (x0 ^Z 0 * y0 ^Z 0)%R
m:Z
x0, y0:R
Hmxy:0 <= m \/ (x0 * y0)%R <> 0%R
n:nat
e:m = n
(x0 * y0) ^Z n = (x0 ^Z n * y0 ^Z n)%R
m:Z
x0, y0:R
Hmxy:0 <= m \/ (x0 * y0)%R <> 0%R
n:nat
Hm:m = - n
(x0 * y0) ^Z (- n) = (x0 ^Z (- n) * y0 ^Z (- n))%R
  -m:Z
x0, y0:R
Hmxy:0 <= m \/ (x0 * y0)%R <> 0%R
e:m = 0
(x0 * y0) ^Z 0 = (x0 ^Z 0 * y0 ^Z 0)%R now simpl; rewrite Rmult_1_l.
  -m:Z
x0, y0:R
Hmxy:0 <= m \/ (x0 * y0)%R <> 0%R
n:nat
e:m = n
(x0 * y0) ^Z n = (x0 ^Z n * y0 ^Z n)%R now rewrite <- !pow_powerRZ, Rpow_mult_distr.
  -m:Z
x0, y0:R
Hmxy:0 <= m \/ (x0 * y0)%R <> 0%R
n:nat
Hm:m = - n
(x0 * y0) ^Z (- n) = (x0 ^Z (- n) * y0 ^Z (- n))%R destruct Hmxy as [H|H].m:Z
x0, y0:R
H:0 <= m
n:nat
Hm:m = - n
(x0 * y0) ^Z (- n) = (x0 ^Z (- n) * y0 ^Z (- n))%R
m:Z
x0, y0:R
H:(x0 * y0)%R <> 0%R
n:nat
Hm:m = - n
(x0 * y0) ^Z (- n) = (x0 ^Z (- n) * y0 ^Z (- n))%R
    +m:Z
x0, y0:R
H:0 <= m
n:nat
Hm:m = - n
(x0 * y0) ^Z (- n) = (x0 ^Z (- n) * y0 ^Z (- n))%R assert(m = 0) as -> by now omega.x0, y0:R
H:0 <= 0
n:nat
Hm:0 = - n
(x0 * y0) ^Z (- n) = (x0 ^Z (- n) * y0 ^Z (- n))%R
      now rewrite <- Hm, Rmult_1_l.
    +m:Z
x0, y0:R
H:(x0 * y0)%R <> 0%R
n:nat
Hm:m = - n
(x0 * y0) ^Z (- n) = (x0 ^Z (- n) * y0 ^Z (- n))%R assert(x0 <> 0)%R by now intros ->; apply H; rewrite Rmult_0_l.m:Z
x0, y0:R
H:(x0 * y0)%R <> 0%R
n:nat
Hm:m = - n
H0:x0 <> 0%R
(x0 * y0) ^Z (- n) = (x0 ^Z (- n) * y0 ^Z (- n))%R
      assert(y0 <> 0)%R by now intros ->; apply H; rewrite Rmult_0_r.m:Z
x0, y0:R
H:(x0 * y0)%R <> 0%R
n:nat
Hm:m = - n
H0:x0 <> 0%R
H1:y0 <> 0%R
(x0 * y0) ^Z (- n) = (x0 ^Z (- n) * y0 ^Z (- n))%R
      rewrite !powerRZ_neg by assumption.m:Z
x0, y0:R
H:(x0 * y0)%R <> 0%R
n:nat
Hm:m = - n
H0:x0 <> 0%R
H1:y0 <> 0%R
(/ (x0 * y0)) ^Z n = ((/ x0) ^Z n * (/ y0) ^Z n)%R
      rewrite Rinv_mult_distr by assumption.m:Z
x0, y0:R
H:(x0 * y0)%R <> 0%R
n:nat
Hm:m = - n
H0:x0 <> 0%R
H1:y0 <> 0%R
(/ x0 * / y0) ^Z n = ((/ x0) ^Z n * (/ y0) ^Z n)%R
      now rewrite <- !pow_powerRZ, Rpow_mult_distr.
Qed.

End PowerRZ.

Local Infix "^Z" := powerRZ (at level 30, right associativity) : R_scope.

(*******************************)
(* For easy interface          *)
(*******************************)
(* decimal_exp r z is defined as r 10^z *)

Definition decimal_exp (r:R) (z:Z) : R := (r * 10 ^Z z).


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

Sum of n first naturals

(*******************************)
(*********)
Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) : nat :=
  match n with
    | O => f 0%nat
    | S n' => (sum_nat_f_O f n' + f (S n'))%nat
  end.

(*********)
Definition sum_nat_f (s n:nat) (f:nat -> nat) : nat :=
  sum_nat_f_O (fun x:nat => f (x + s)%nat) (n - s).

(*********)
Definition sum_nat_O (n:nat) : nat := sum_nat_f_O (fun x:nat => x) n.

(*********)
Definition sum_nat (s n:nat) : nat := sum_nat_f s n (fun x:nat => x).

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

Sum

(*******************************)
(*********)
Fixpoint sum_f_R0 (f:nat -> R) (N:nat) : R :=
  match N with
    | O => f 0%nat
    | S i => sum_f_R0 f i + f (S i)
  end.

(*********)
Definition sum_f (s n:nat) (f:nat -> R) : R :=
  sum_f_R0 (fun x:nat => f (x + s)%nat) (n - s).

Lemma GP_finite :
  forall (x:R) (n:nat),
    sum_f_R0 (fun n:nat => x ^ n) n * (x - 1) = x ^ (n + 1) - 1.forall (x : R) (n : nat),
sum_f_R0 (fun n0 : nat => x ^ n0) n * (x - 1) =
x ^ (n + 1) - 1
Proof.forall (x : R) (n : nat),
sum_f_R0 (fun n0 : nat => x ^ n0) n * (x - 1) =
x ^ (n + 1) - 1
  intros; induction  n as [| n Hrecn]; simpl.x:R
1 * (x - 1) = x * 1 - 1
x:R
n:nat
Hrecn:sum_f_R0 (fun n0 : nat => x ^ n0) n * (x - 1) =
x ^ (n + 1) - 1
(sum_f_R0 (fun n0 : nat => x ^ n0) n + x * x ^ n) *
(x - 1) = x * x ^ (n + 1) - 1
  ring.x:R
n:nat
Hrecn:sum_f_R0 (fun n0 : nat => x ^ n0) n * (x - 1) =
x ^ (n + 1) - 1
(sum_f_R0 (fun n0 : nat => x ^ n0) n + x * x ^ n) *
(x - 1) = x * x ^ (n + 1) - 1
  rewrite Rmult_plus_distr_r; rewrite Hrecn; cut ((n + 1)%nat = S n).x:R
n:nat
Hrecn:sum_f_R0 (fun n0 : nat => x ^ n0) n * (x - 1) =
x ^ (n + 1) - 1
(n + 1)%nat = S n ->
x ^ (n + 1) - 1 + x * x ^ n * (x - 1) =
x * x ^ (n + 1) - 1
x:R
n:nat
Hrecn:sum_f_R0 (fun n0 : nat => x ^ n0) n * (x - 1) =
x ^ (n + 1) - 1
(n + 1)%nat = S n
  intro H; rewrite H; simpl; ring.x:R
n:nat
Hrecn:sum_f_R0 (fun n0 : nat => x ^ n0) n * (x - 1) =
x ^ (n + 1) - 1
(n + 1)%nat = S n
  omega.
Qed.

Lemma sum_f_R0_triangle :
  forall (x:nat -> R) (n:nat),
    Rabs (sum_f_R0 x n) <= sum_f_R0 (fun i:nat => Rabs (x i)) n.forall (x : nat -> R) (n : nat),
Rabs (sum_f_R0 x n) <=
sum_f_R0 (fun i : nat => Rabs (x i)) n
Proof.forall (x : nat -> R) (n : nat),
Rabs (sum_f_R0 x n) <=
sum_f_R0 (fun i : nat => Rabs (x i)) n
  intro; simple induction n; simpl.x:nat -> R
n:nat
Rabs (x 0%nat) <= Rabs (x 0%nat)
x:nat -> R
n:nat
forall n0 : nat,
Rabs (sum_f_R0 x n0) <=
sum_f_R0 (fun i : nat => Rabs (x i)) n0 ->
Rabs (sum_f_R0 x n0 + x (S n0)) <=
sum_f_R0 (fun i : nat => Rabs (x i)) n0 +
Rabs (x (S n0))
  unfold Rle; right; reflexivity.x:nat -> R
n:nat
forall n0 : nat,
Rabs (sum_f_R0 x n0) <=
sum_f_R0 (fun i : nat => Rabs (x i)) n0 ->
Rabs (sum_f_R0 x n0 + x (S n0)) <=
sum_f_R0 (fun i : nat => Rabs (x i)) n0 +
Rabs (x (S n0))
  intro m; intro;
    apply
      (Rle_trans (Rabs (sum_f_R0 x m + x (S m)))
        (Rabs (sum_f_R0 x m) + Rabs (x (S m)))
        (sum_f_R0 (fun i:nat => Rabs (x i)) m + Rabs (x (S m)))).x:nat -> R
n, m:nat
H:Rabs (sum_f_R0 x m) <=
sum_f_R0 (fun i : nat => Rabs (x i)) m
Rabs (sum_f_R0 x m + x (S m)) <=
Rabs (sum_f_R0 x m) + Rabs (x (S m))
x:nat -> R
n, m:nat
H:Rabs (sum_f_R0 x m) <=
sum_f_R0 (fun i : nat => Rabs (x i)) m
Rabs (sum_f_R0 x m) + Rabs (x (S m)) <=
sum_f_R0 (fun i : nat => Rabs (x i)) m +
Rabs (x (S m))
  apply Rabs_triang.x:nat -> R
n, m:nat
H:Rabs (sum_f_R0 x m) <=
sum_f_R0 (fun i : nat => Rabs (x i)) m
Rabs (sum_f_R0 x m) + Rabs (x (S m)) <=
sum_f_R0 (fun i : nat => Rabs (x i)) m +
Rabs (x (S m))
  rewrite Rplus_comm;
    rewrite (Rplus_comm (sum_f_R0 (fun i:nat => Rabs (x i)) m) (Rabs (x (S m))));
      apply Rplus_le_compat_l; assumption.
Qed.

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

Distance in R

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

(*********)
Definition R_dist (x y:R) : R := Rabs (x - y).

(*********)
Lemma R_dist_pos : forall x y:R, R_dist x y >= 0.forall x y : R, R_dist x y >= 0
Proof.forall x y : R, R_dist x y >= 0
  intros; unfold R_dist; unfold Rabs; case (Rcase_abs (x - y));
    intro l.x, y:R
l:x - y < 0
- (x - y) >= 0
x, y:R
l:x - y >= 0
x - y >= 0
  unfold Rge; left; apply (Ropp_gt_lt_0_contravar (x - y) l).x, y:R
l:x - y >= 0
x - y >= 0
  trivial.
Qed.

(*********)
Lemma R_dist_sym : forall x y:R, R_dist x y = R_dist y x.forall x y : R, R_dist x y = R_dist y x
Proof.forall x y : R, R_dist x y = R_dist y x
  unfold R_dist; intros; split_Rabs; try ring.x, y:R
Hlt:x - y < 0
Hlt0:y - x < 0
- (x - y) = - (y - x)
x, y:R
Hge:x - y >= 0
Hge0:y - x >= 0
x - y = y - x
  generalize (Ropp_gt_lt_0_contravar (y - x) Hlt0); intro;
    rewrite (Ropp_minus_distr y x) in H; generalize (Rlt_asym (x - y) 0 Hlt);
      intro; unfold Rgt in H; exfalso; auto.x, y:R
Hge:x - y >= 0
Hge0:y - x >= 0
x - y = y - x
  generalize (minus_Rge y x Hge0); intro; generalize (minus_Rge x y Hge); intro;
    generalize (Rge_antisym x y H0 H); intro; rewrite H1;
      ring.
Qed.

(*********)
Lemma R_dist_refl : forall x y:R, R_dist x y = 0 <-> x = y.forall x y : R, R_dist x y = 0 <-> x = y
Proof.forall x y : R, R_dist x y = 0 <-> x = y
  unfold R_dist; intros; split_Rabs; split; intros.x, y:R
Hlt:x - y < 0
H:- (x - y) = 0
x = y
x, y:R
Hlt:x - y < 0
H:x = y
- (x - y) = 0
x, y:R
Hge:x - y >= 0
H:x - y = 0
x = y
x, y:R
Hge:x - y >= 0
H:x = y
x - y = 0
  rewrite (Ropp_minus_distr x y) in H; symmetry;
    apply (Rminus_diag_uniq y x H).x, y:R
Hlt:x - y < 0
H:x = y
- (x - y) = 0
x, y:R
Hge:x - y >= 0
H:x - y = 0
x = y
x, y:R
Hge:x - y >= 0
H:x = y
x - y = 0
  rewrite (Ropp_minus_distr x y); generalize (eq_sym H); intro;
    apply (Rminus_diag_eq y x H0).x, y:R
Hge:x - y >= 0
H:x - y = 0
x = y
x, y:R
Hge:x - y >= 0
H:x = y
x - y = 0
  apply (Rminus_diag_uniq x y H).x, y:R
Hge:x - y >= 0
H:x = y
x - y = 0
  apply (Rminus_diag_eq x y H).
Qed.

Lemma R_dist_eq : forall x:R, R_dist x x = 0.forall x : R, R_dist x x = 0
Proof.forall x : R, R_dist x x = 0
  unfold R_dist; intros; split_Rabs; intros; ring.
Qed.

(***********)
Lemma R_dist_tri : forall x y z:R, R_dist x y <= R_dist x z + R_dist z y.forall x y z : R,
R_dist x y <= R_dist x z + R_dist z y
Proof.forall x y z : R,
R_dist x y <= R_dist x z + R_dist z y
  intros; unfold R_dist; replace (x - y) with (x - z + (z - y));
    [ apply (Rabs_triang (x - z) (z - y)) | ring ].
Qed.

(*********)
Lemma R_dist_plus :
  forall a b c d:R, R_dist (a + c) (b + d) <= R_dist a b + R_dist c d.forall a b c d : R,
R_dist (a + c) (b + d) <= R_dist a b + R_dist c d
Proof.forall a b c d : R,
R_dist (a + c) (b + d) <= R_dist a b + R_dist c d
  intros; unfold R_dist;
    replace (a + c - (b + d)) with (a - b + (c - d)).a, b, c, d:R
Rabs (a - b + (c - d)) <= Rabs (a - b) + Rabs (c - d)
a, b, c, d:R
a - b + (c - d) = a + c - (b + d)
  exact (Rabs_triang (a - b) (c - d)).a, b, c, d:R
a - b + (c - d) = a + c - (b + d)
  ring.
Qed.

Lemma R_dist_mult_l : forall a b c,
  R_dist (a * b) (a * c) = Rabs a * R_dist b c.forall a b c : R,
R_dist (a * b) (a * c) = Rabs a * R_dist b c
Proof.forall a b c : R,
R_dist (a * b) (a * c) = Rabs a * R_dist b c
unfold R_dist.forall a b c : R,
Rabs (a * b - a * c) = Rabs a * Rabs (b - c) 
intros a b c; rewrite <- Rmult_minus_distr_l, Rabs_mult; reflexivity.
Qed.

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

Infinite Sum

(*******************************)
(*********)
Definition infinite_sum (s:nat -> R) (l:R) : Prop :=
  forall eps:R,
    eps > 0 ->
    exists N : nat,
      (forall n:nat, (n >= N)%nat -> R_dist (sum_f_R0 s n) l < eps).

Compatibility with previous versions

Notation infinit_sum := infinite_sum (only parsing).