(****************************************************************************
                                                                             
          IEEE754  :  Rpow                                                 
                                                                             
          Laurent Thery                                                      
                                                                             
  *****************************************************************************
  Definition of an exponential function over relative numbers *)
Require Export Omega.
Require Export Digit.
(* We have already an exponential over natural number,
   we prove some basic properties for this function *)
 
Theorem pow_O : forall e : R, (e ^ 0)%R = 1%R.
(* Goal: forall e : R, @eq R (powerRZ e (Z.succ Z0)) e *)
simpl in |- *; auto with real.
Qed.
 
Theorem pow_1 : forall e : R, (e ^ 1)%R = e.
(* Goal: forall e : R, @eq R (powerRZ e (Z.succ Z0)) e *)
simpl in |- *; auto with real.
Qed.
 
Theorem pow_NR0 : forall (e : R) (n : nat), e <> 0%R -> (e ^ n)%R <> 0%R.
(* Goal: forall e : R, @eq R (powerRZ e (Z.succ Z0)) e *)
intros e n; elim n; simpl in |- *; auto with real.
Qed.
 
Theorem pow_add :
 forall (e : R) (n m : nat), (e ^ (n + m))%R = (e ^ n * e ^ m)%R.
(* Goal: forall e : R, @eq R (powerRZ e (Z.succ Z0)) e *)
intros e n; elim n; simpl in |- *; auto with real.
(* Goal: forall (n : nat) (_ : forall m : nat, @eq R (pow e (Init.Nat.add n m)) (Rmult (pow e n) (pow e m))) (m : nat), @eq R (Rmult e (pow e (Init.Nat.add n m))) (Rmult (Rmult e (pow e n)) (pow e m)) *)
intros n0 H' m; rewrite H'; auto with real.
Qed.
Hint Resolve pow_O pow_1 pow_NR0 pow_add: real.
 
Theorem pow_RN_plus :
 forall (e : R) (n m : nat),
 e <> 0%R -> (e ^ n)%R = (e ^ (n + m) * / e ^ m)%R.
(* Goal: forall e : R, @eq R (powerRZ e (Z.succ Z0)) e *)
intros e n; elim n; simpl in |- *; auto with real.
(* Goal: forall (n : nat) (_ : forall (m : nat) (_ : not (@eq R e (IZR Z0))), @eq R (pow e n) (Rmult (pow e (Init.Nat.add n m)) (Rinv (pow e m)))) (m : nat) (_ : not (@eq R e (IZR Z0))), @eq R (Rmult e (pow e n)) (Rmult (Rmult e (pow e (Init.Nat.add n m))) (Rinv (pow e m))) *)
intros n0 H' m H'0.
(* Goal: @eq R (Rmult e (pow e n0)) (Rmult (Rmult e (pow e (Init.Nat.add n0 m))) (Rinv (pow e m))) *)
rewrite Rmult_assoc; rewrite <- H'; auto.
Qed.
 
Theorem pow_lt : forall (e : R) (n : nat), (0 < e)%R -> (0 < e ^ n)%R.
(* Goal: forall e : R, @eq R (powerRZ e (Z.succ Z0)) e *)
intros e n; elim n; simpl in |- *; auto with real.
(* Goal: forall (n : nat) (_ : forall _ : Rlt (IZR Z0) e, Rlt (IZR Z0) (pow e n)) (_ : Rlt (IZR Z0) e), Rlt (IZR Z0) (Rmult e (pow e n)) *)
intros n0 H' H'0; replace 0%R with (e * 0)%R; auto with real.
Qed.
Hint Resolve pow_lt: real.
 
Theorem Rlt_pow_R1 :
 forall (e : R) (n : nat), (1 < e)%R -> 0 < n -> (1 < e ^ n)%R.
(* Goal: forall e : R, @eq R (powerRZ e (Z.succ Z0)) e *)
intros e n; elim n; simpl in |- *; auto with real.
(* Goal: forall (_ : Rlt (IZR (Zpos xH)) e) (_ : lt O O), Rlt (IZR (Zpos xH)) (IZR (Zpos xH)) *)
(* Goal: forall (n : nat) (_ : forall (_ : Rlt (IZR (Zpos xH)) e) (_ : lt O n), Rlt (IZR (Zpos xH)) (pow e n)) (_ : Rlt (IZR (Zpos xH)) e) (_ : lt O (S n)), Rlt (IZR (Zpos xH)) (Rmult e (pow e n)) *)
intros H' H'0; Contradict H'0; auto with arith.
(* Goal: forall (n : nat) (_ : forall (_ : Rlt (IZR (Zpos xH)) e) (_ : lt O n), Rlt (IZR (Zpos xH)) (pow e n)) (_ : Rlt (IZR (Zpos xH)) e) (_ : lt O (S n)), Rlt (IZR (Zpos xH)) (Rmult e (pow e n)) *)
intros n0; case n0.
(* Goal: forall (_ : forall (_ : Rlt (IZR (Zpos xH)) e) (_ : lt O O), Rlt (IZR (Zpos xH)) (pow e O)) (_ : Rlt (IZR (Zpos xH)) e) (_ : lt O (S O)), Rlt (IZR (Zpos xH)) (Rmult e (pow e O)) *)
(* Goal: forall (n : nat) (_ : forall (_ : Rlt (IZR (Zpos xH)) e) (_ : lt O (S n)), Rlt (IZR (Zpos xH)) (pow e (S n))) (_ : Rlt (IZR (Zpos xH)) e) (_ : lt O (S (S n))), Rlt (IZR (Zpos xH)) (Rmult e (pow e (S n))) *)
simpl in |- *; rewrite Rmult_1_r; auto.
(* Goal: forall (n : nat) (_ : forall (_ : Rlt (IZR (Zpos xH)) e) (_ : lt O (S n)), Rlt (IZR (Zpos xH)) (pow e (S n))) (_ : Rlt (IZR (Zpos xH)) e) (_ : lt O (S (S n))), Rlt (IZR (Zpos xH)) (Rmult e (pow e (S n))) *)
intros n1 H' H'0 H'1.
(* Goal: Rlt (IZR (Zpos xH)) (Rmult e (pow e (S n1))) *)
replace 1%R with (1 * 1)%R; auto with real.
(* Goal: Rlt (Rmult (IZR (Zpos xH)) (IZR (Zpos xH))) (Rmult e (pow e (S n1))) *)
apply Rlt_trans with (r2 := (e * 1)%R); auto with real.
(* Goal: Rlt (Rmult (pow e n) (Rminus (IZR (Zpos xH)) (pow e (Init.Nat.sub m n)))) (Rmult (pow e n) (IZR Z0)) *)
(* Goal: @eq nat (Init.Nat.add (Init.Nat.sub m n) n) m *)
apply Rmult_lt_compat_l; auto with real.
(* Goal: Rlt (IZR Z0) e *)
(* Goal: Rlt (Rminus (IZR (Zpos xH)) (pow e (Init.Nat.sub m n))) (IZR Z0) *)
(* Goal: @eq nat (Init.Nat.add (Init.Nat.sub m n) n) m *)
apply Rlt_trans with (r2 := 1%R); auto with real.
(* Goal: Rlt (IZR (Zpos xH)) (pow e (S n1)) *)
apply H'; auto with arith.
Qed.
Hint Resolve Rlt_pow_R1: real.
 
Theorem Rlt_pow :
 forall (e : R) (n m : nat), (1 < e)%R -> n < m -> (e ^ n < e ^ m)%R.
(* Goal: forall (e : R) (n m : nat) (_ : Rlt (IZR (Zpos xH)) e) (_ : lt n m), Rlt (pow e n) (pow e m) *)
intros e n m H' H'0; replace m with (m - n + n).
(* Goal: Rlt (pow e n) (pow e (Init.Nat.add (Init.Nat.sub m n) n)) *)
(* Goal: @eq nat (Init.Nat.add (Init.Nat.sub m n) n) m *)
rewrite pow_add.
pattern (e ^ n)%R at 1 in |- *; replace (e ^ n)%R with (1 * e ^ n)%R;
 auto with real.
(* Goal: Rlt (Rmult (IZR (Zpos xH)) (pow e n)) (Rmult (pow e (Init.Nat.sub m n)) (pow e n)) *)
(* Goal: @eq nat (Init.Nat.add (Init.Nat.sub m n) n) m *)
apply Rminus_lt.
repeat rewrite (fun x : R => Rmult_comm x (e ^ n));
 rewrite <- Rmult_minus_distr_l.
(* Goal: Rlt (Rmult (pow e n) (Rminus (IZR (Zpos xH)) (pow e (Init.Nat.sub m n)))) (IZR Z0) *)
(* Goal: @eq nat (Init.Nat.add (Init.Nat.sub m n) n) m *)
replace 0%R with (e ^ n * 0)%R; auto with real.
(* Goal: Rlt (Rmult (pow e n) (Rminus (IZR (Zpos xH)) (pow e (Init.Nat.sub m n)))) (Rmult (pow e n) (IZR Z0)) *)
(* Goal: @eq nat (Init.Nat.add (Init.Nat.sub m n) n) m *)
apply Rmult_lt_compat_l; auto with real.
(* Goal: Rlt (IZR Z0) (pow e n) *)
(* Goal: Rlt (Rminus (IZR (Zpos xH)) (pow e (Init.Nat.sub m n))) (IZR Z0) *)
(* Goal: @eq nat (Init.Nat.add (Init.Nat.sub m n) n) m *)
apply pow_lt; auto with real.
(* Goal: Rlt (IZR Z0) e *)
(* Goal: Rlt (Rminus (IZR (Zpos xH)) (pow e (Init.Nat.sub m n))) (IZR Z0) *)
(* Goal: @eq nat (Init.Nat.add (Init.Nat.sub m n) n) m *)
apply Rlt_trans with (r2 := 1%R); auto with real.
(* Goal: Rlt (Rminus (IZR (Zpos xH)) (pow e (Init.Nat.sub m n))) (IZR Z0) *)
(* Goal: @eq nat (Init.Nat.add (Init.Nat.sub m n) n) m *)
apply Rlt_minus; auto with real.
(* Goal: Rlt (IZR (Zpos xH)) (pow e (Init.Nat.sub m n)) *)
(* Goal: @eq nat (Init.Nat.add (Init.Nat.sub m n) n) m *)
apply Rlt_pow_R1; auto with arith.
(* Goal: lt O (Init.Nat.sub m n) *)
(* Goal: @eq nat (Init.Nat.add (Init.Nat.sub m n) n) m *)
apply plus_lt_reg_l with (p := n); auto with arith.
(* Goal: lt (Init.Nat.add n O) (Init.Nat.add n (Init.Nat.sub m n)) *)
(* Goal: @eq nat (Init.Nat.add (Init.Nat.sub m n) n) m *)
rewrite le_plus_minus_r; auto with arith; rewrite <- plus_n_O; auto.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.sub m n) n) m *)
rewrite plus_comm; auto with arith.
Qed.
Hint Resolve Rlt_pow: real.
 
Theorem pow_R1 :
 forall (r : R) (n : nat), (r ^ n)%R = 1%R -> Rabs r = 1%R \/ n = 0.
intros r n H'.
case (Req_dec (Rabs r) 1); auto; intros H'1.
case (Rdichotomy _ _ H'1); intros H'2.
generalize H'; case n; auto.
intros n0 H'0.
cut (r <> 0%R); [ intros Eq1 | idtac ].
2: Contradict H'0; auto with arith.
2: simpl in |- *; rewrite H'0; rewrite Rmult_0_l; auto with real.
cut (Rabs r <> 0%R); [ intros Eq2 | apply Rabs_no_R0 ]; auto.
absurd (Rabs (/ r) ^ 0 < Rabs (/ r) ^ S n0)%R; auto.
replace (Rabs (/ r) ^ S n0)%R with 1%R.
simpl in |- *; apply Rlt_irrefl; auto.
rewrite Rabs_Rinv; auto.
rewrite <- Rinv_pow; auto.
rewrite RPow_abs; auto.
rewrite H'0; rewrite Rabs_right; auto with real.
apply Rlt_pow; auto with arith.
rewrite Rabs_Rinv; auto.
apply Rmult_lt_reg_l with (r := Rabs r).
case (Rabs_pos r); auto.
intros H'3; case Eq2; auto.
rewrite Rmult_1_r; rewrite Rinv_r; auto with real.
generalize H'; case n; auto.
intros n0 H'0.
cut (r <> 0%R); [ intros Eq1 | auto with real ].
2: Contradict H'0; simpl in |- *; rewrite H'0; rewrite Rmult_0_l;
    auto with real.
cut (Rabs r <> 0%R); [ intros Eq2 | apply Rabs_no_R0 ]; auto.
absurd (Rabs r ^ 0 < Rabs r ^ S n0)%R; auto with real arith.
(* Goal: forall e : R, @eq R (powerRZ e (Z.succ Z0)) e *)
repeat rewrite RPow_abs; rewrite H'0; simpl in |- *; auto with real.
Qed.
 
Theorem Zpower_NR0 :
 forall (e : Z) (n : nat), (0 <= e)%Z -> (0 <= Zpower_nat e n)%Z.
intros e n; elim n; unfold Zpower_nat in |- *; simpl in |- *;
(* Goal: @eq Z (Z.add n (Z.succ Z0)) (Z.succ n) *)
 auto with zarith.
Qed.
 
Theorem Zpower_NR1 :
 forall (e : Z) (n : nat), (1 <= e)%Z -> (1 <= Zpower_nat e n)%Z.
intros e n; elim n; unfold Zpower_nat in |- *; simpl in |- *;
(* Goal: @eq Z (Z.add n (Z.succ Z0)) (Z.succ n) *)
 auto with zarith.
Qed.
Hint Resolve Zpower_NR0 Zpower_NR1: zarith.
(* To define exponential over relative number, we simply do 
   a case analysis on the sign of the number *)
 
(*Definition powerRZ :=
   [e : R] [n : Z]  Cases n of
                      ZERO => R1
                     | (POS p) => (pow e (convert p))
                     | (NEG p) => (Rinv (pow e (convert p)))
                    end.*)
(* we now prove some basic properties of our exponential *)
 
Theorem powerRZ_O : forall e : R, powerRZ e 0 = 1%R.
(* Goal: forall e : R, @eq R (powerRZ e Z0) (IZR (Zpos xH)) *)
simpl in |- *; auto.
Qed.
 
Theorem powerRZ_1 : forall e : R, powerRZ e (Zsucc 0) = e.
(* Goal: forall e : R, @eq R (powerRZ e (Z.succ Z0)) e *)
simpl in |- *; auto with real.
Qed.
 
Theorem powerRZ_NOR : forall (e : R) (z : Z), e <> 0%R -> powerRZ e z <> 0%R.
(* Goal: forall e : R, @eq R (powerRZ e (Z.succ Z0)) e *)
intros e z; case z; simpl in |- *; auto with real.
Qed.
Hint Resolve powerRZ_O powerRZ_1 powerRZ_NOR: real.
 
Theorem powerRZ_add :
 forall (e : R) (n m : Z),
 e <> 0%R -> powerRZ e (n + m) = (powerRZ e n * powerRZ e m)%R.
(* Goal: forall e : R, @eq R (powerRZ e (Z.succ Z0)) e *)
intros e n m; case n; case m; simpl in |- *; auto with real.
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
intros n1 m1; rewrite nat_of_P_plus_morphism; auto with real.
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (powerRZ e (Z.pos_sub p p0)) (Rmult (Rinv (pow e (Pos.to_nat p0))) (pow e (Pos.to_nat p))) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
intros n1 m1. rewrite Z.pos_sub_spec; unfold Pos.compare.
(* Goal: forall e : R, @eq R (powerRZ e (Z.succ Z0)) e *)
CaseEq (Pcompare m1 n1 Datatypes.Eq); simpl in |- *; auto with real.
(* Goal: forall (_ : @eq comparison (Pos.compare_cont Eq n1 m1) Eq) (_ : not (@eq R e (IZR Z0))), @eq R (IZR (Zpos xH)) (Rmult (Rinv (pow e (Pos.to_nat m1))) (pow e (Pos.to_nat n1))) *)
(* Goal: forall (_ : @eq comparison (Pos.compare_cont Eq n1 m1) Lt) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.sub m1 n1)))) (Rmult (Rinv (pow e (Pos.to_nat m1))) (pow e (Pos.to_nat n1))) *)
(* Goal: forall (_ : @eq comparison (Pos.compare_cont Eq n1 m1) Gt) (_ : not (@eq R e (IZR Z0))), @eq R (pow e (Pos.to_nat (Pos.sub n1 m1))) (Rmult (Rinv (pow e (Pos.to_nat m1))) (pow e (Pos.to_nat n1))) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
intros H' H'0; rewrite Pcompare_Eq_eq with (1 := H'); auto with real.
(* Goal: forall (_ : @eq comparison (Pos.compare_cont Eq n1 m1) Gt) (_ : not (@eq R e (IZR Z0))), @eq R (pow e (Pos.to_nat (Pos.sub n1 m1))) (Rmult (Rinv (pow e (Pos.to_nat m1))) (pow e (Pos.to_nat n1))) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
intros H' H'0; rewrite (nat_of_P_minus_morphism n1 m1); auto with real.
rewrite (pow_RN_plus e (nat_of_P n1 - nat_of_P m1) (nat_of_P m1));
 auto with real.
(* Goal: @eq R (Rmult (pow e (Init.Nat.add (Init.Nat.sub (Pos.to_nat n1) (Pos.to_nat m1)) (Pos.to_nat m1))) (Rinv (pow e (Pos.to_nat m1)))) (Rmult (Rinv (pow e (Pos.to_nat m1))) (pow e (Pos.to_nat n1))) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
rewrite plus_comm; rewrite le_plus_minus_r; auto with real.
(* Goal: @eq R (Rinv (Rmult (pow e (Pos.to_nat m1)) (Rinv (pow e (Pos.to_nat n1))))) (Rmult (Rinv (pow e (Pos.to_nat m1))) (pow e (Pos.to_nat n1))) *)
(* Goal: le (Pos.to_nat n1) (Pos.to_nat m1) *)
(* Goal: @eq comparison (Pos.compare_cont Eq m1 n1) Gt *)
(* Goal: forall (_ : @eq comparison (Pos.compare_cont Eq n1 m1) Gt) (_ : not (@eq R e (IZR Z0))), @eq R (pow e (Pos.to_nat (Pos.sub n1 m1))) (Rmult (Rinv (pow e (Pos.to_nat m1))) (pow e (Pos.to_nat n1))) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
rewrite Rinv_mult_distr; auto with real.
(* Goal: @eq R (Rmult (Rinv (pow e (Pos.to_nat n1))) (Rinv (Rinv (pow e (Pos.to_nat m1))))) (Rmult (pow e (Pos.to_nat m1)) (Rinv (pow e (Pos.to_nat n1)))) *)
(* Goal: le (Pos.to_nat m1) (Pos.to_nat n1) *)
(* Goal: @eq comparison (Pos.compare_cont Eq n1 m1) Gt *)
(* Goal: forall (_ : @eq comparison (Pos.compare_cont Eq m1 n1) Gt) (_ : not (@eq R e (IZR Z0))), @eq R (pow e (Pos.to_nat (Pos.sub m1 n1))) (Rmult (pow e (Pos.to_nat m1)) (Rinv (pow e (Pos.to_nat n1)))) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (powerRZ e (Z.pos_sub p p0)) (Rmult (Rinv (pow e (Pos.to_nat p0))) (pow e (Pos.to_nat p))) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
rewrite Rinv_involutive; auto with real.
(* Goal: le (Pos.to_nat m1) (Pos.to_nat n1) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
apply lt_le_weak.
(* Goal: lt (Pos.to_nat p0) (Pos.to_nat p) *)
(* Goal: forall (p : positive) (_ : Rlt (IZR (Zpos xH)) e) (_ : Z.lt (Zneg p) Z0), Rlt (Rinv (pow e (Pos.to_nat p))) (IZR (Zpos xH)) *)
(* Goal: forall (p p0 : positive) (_ : Rlt (IZR (Zpos xH)) e) (_ : Z.lt (Zneg p0) (Zpos p)), Rlt (Rinv (pow e (Pos.to_nat p0))) (pow e (Pos.to_nat p)) *)
(* Goal: forall (p p0 : positive) (_ : Rlt (IZR (Zpos xH)) e) (_ : Z.lt (Zneg p0) (Zneg p)), Rlt (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p))) *)
apply nat_of_P_lt_Lt_compare_morphism; auto.
(* Goal: @eq comparison (Pos.compare_cont Eq m1 n1) Gt *)
(* Goal: forall (_ : @eq comparison (Pos.compare_cont Eq n1 m1) Gt) (_ : not (@eq R e (IZR Z0))), @eq R (pow e (Pos.to_nat (Pos.sub n1 m1))) (Rmult (Rinv (pow e (Pos.to_nat m1))) (pow e (Pos.to_nat n1))) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
apply ZC2; auto.
(* Goal: forall (_ : @eq comparison (Pos.compare_cont Eq n1 m1) Lt) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.sub m1 n1)))) (Rmult (Rinv (pow e (Pos.to_nat m1))) (pow e (Pos.to_nat n1))) *)
(* Goal: forall (_ : @eq comparison (Pos.compare_cont Eq n1 m1) Gt) (_ : not (@eq R e (IZR Z0))), @eq R (pow e (Pos.to_nat (Pos.sub n1 m1))) (Rmult (Rinv (pow e (Pos.to_nat m1))) (pow e (Pos.to_nat n1))) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
intros H' H'0; rewrite (nat_of_P_minus_morphism m1 n1); auto with real.
rewrite (pow_RN_plus e (nat_of_P m1 - nat_of_P n1) (nat_of_P n1));
 auto with real.
(* Goal: @eq R (Rmult (pow e (Init.Nat.add (Init.Nat.sub (Pos.to_nat n1) (Pos.to_nat m1)) (Pos.to_nat m1))) (Rinv (pow e (Pos.to_nat m1)))) (Rmult (Rinv (pow e (Pos.to_nat m1))) (pow e (Pos.to_nat n1))) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
rewrite plus_comm; rewrite le_plus_minus_r; auto with real.
(* Goal: le (Pos.to_nat m1) (Pos.to_nat n1) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
apply lt_le_weak.
(* Goal: lt (Pos.to_nat n1) (Pos.to_nat m1) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (powerRZ e (Z.pos_sub p p0)) (Rmult (Rinv (pow e (Pos.to_nat p0))) (pow e (Pos.to_nat p))) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
change (nat_of_P m1 > nat_of_P n1) in |- *.
(* Goal: gt (Pos.to_nat n1) (Pos.to_nat m1) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
apply nat_of_P_gt_Gt_compare_morphism; auto.
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (powerRZ e (Z.pos_sub p p0)) (Rmult (Rinv (pow e (Pos.to_nat p0))) (pow e (Pos.to_nat p))) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
intros n1 m1. rewrite Z.pos_sub_spec; unfold Pos.compare.
(* Goal: forall e : R, @eq R (powerRZ e (Z.succ Z0)) e *)
CaseEq (Pcompare n1 m1 Datatypes.Eq); simpl in |- *; auto with real.
(* Goal: forall (_ : @eq comparison (Pos.compare_cont Eq n1 m1) Eq) (_ : not (@eq R e (IZR Z0))), @eq R (IZR (Zpos xH)) (Rmult (Rinv (pow e (Pos.to_nat m1))) (pow e (Pos.to_nat n1))) *)
(* Goal: forall (_ : @eq comparison (Pos.compare_cont Eq n1 m1) Lt) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.sub m1 n1)))) (Rmult (Rinv (pow e (Pos.to_nat m1))) (pow e (Pos.to_nat n1))) *)
(* Goal: forall (_ : @eq comparison (Pos.compare_cont Eq n1 m1) Gt) (_ : not (@eq R e (IZR Z0))), @eq R (pow e (Pos.to_nat (Pos.sub n1 m1))) (Rmult (Rinv (pow e (Pos.to_nat m1))) (pow e (Pos.to_nat n1))) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
intros H' H'0; rewrite Pcompare_Eq_eq with (1 := H'); auto with real.
(* Goal: forall (_ : @eq comparison (Pos.compare_cont Eq n1 m1) Lt) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.sub m1 n1)))) (Rmult (Rinv (pow e (Pos.to_nat m1))) (pow e (Pos.to_nat n1))) *)
(* Goal: forall (_ : @eq comparison (Pos.compare_cont Eq n1 m1) Gt) (_ : not (@eq R e (IZR Z0))), @eq R (pow e (Pos.to_nat (Pos.sub n1 m1))) (Rmult (Rinv (pow e (Pos.to_nat m1))) (pow e (Pos.to_nat n1))) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
intros H' H'0; rewrite (nat_of_P_minus_morphism m1 n1); auto with real.
rewrite (pow_RN_plus e (nat_of_P m1 - nat_of_P n1) (nat_of_P n1));
 auto with real.
(* Goal: @eq R (Rmult (pow e (Init.Nat.add (Init.Nat.sub (Pos.to_nat n1) (Pos.to_nat m1)) (Pos.to_nat m1))) (Rinv (pow e (Pos.to_nat m1)))) (Rmult (Rinv (pow e (Pos.to_nat m1))) (pow e (Pos.to_nat n1))) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
rewrite plus_comm; rewrite le_plus_minus_r; auto with real.
(* Goal: @eq R (Rinv (Rmult (pow e (Pos.to_nat m1)) (Rinv (pow e (Pos.to_nat n1))))) (Rmult (Rinv (pow e (Pos.to_nat m1))) (pow e (Pos.to_nat n1))) *)
(* Goal: le (Pos.to_nat n1) (Pos.to_nat m1) *)
(* Goal: @eq comparison (Pos.compare_cont Eq m1 n1) Gt *)
(* Goal: forall (_ : @eq comparison (Pos.compare_cont Eq n1 m1) Gt) (_ : not (@eq R e (IZR Z0))), @eq R (pow e (Pos.to_nat (Pos.sub n1 m1))) (Rmult (Rinv (pow e (Pos.to_nat m1))) (pow e (Pos.to_nat n1))) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
rewrite Rinv_mult_distr; auto with real.
(* Goal: le (Pos.to_nat m1) (Pos.to_nat n1) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
apply lt_le_weak.
(* Goal: lt (Pos.to_nat p0) (Pos.to_nat p) *)
(* Goal: forall (p : positive) (_ : Rlt (IZR (Zpos xH)) e) (_ : Z.lt (Zneg p) Z0), Rlt (Rinv (pow e (Pos.to_nat p))) (IZR (Zpos xH)) *)
(* Goal: forall (p p0 : positive) (_ : Rlt (IZR (Zpos xH)) e) (_ : Z.lt (Zneg p0) (Zpos p)), Rlt (Rinv (pow e (Pos.to_nat p0))) (pow e (Pos.to_nat p)) *)
(* Goal: forall (p p0 : positive) (_ : Rlt (IZR (Zpos xH)) e) (_ : Z.lt (Zneg p0) (Zneg p)), Rlt (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p))) *)
apply nat_of_P_lt_Lt_compare_morphism; auto.
(* Goal: @eq comparison (Pos.compare_cont Eq m1 n1) Gt *)
(* Goal: forall (_ : @eq comparison (Pos.compare_cont Eq n1 m1) Gt) (_ : not (@eq R e (IZR Z0))), @eq R (pow e (Pos.to_nat (Pos.sub n1 m1))) (Rmult (Rinv (pow e (Pos.to_nat m1))) (pow e (Pos.to_nat n1))) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
apply ZC2; auto.
(* Goal: forall (_ : @eq comparison (Pos.compare_cont Eq n1 m1) Gt) (_ : not (@eq R e (IZR Z0))), @eq R (pow e (Pos.to_nat (Pos.sub n1 m1))) (Rmult (Rinv (pow e (Pos.to_nat m1))) (pow e (Pos.to_nat n1))) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
intros H' H'0; rewrite (nat_of_P_minus_morphism n1 m1); auto with real.
rewrite (pow_RN_plus e (nat_of_P n1 - nat_of_P m1) (nat_of_P m1));
 auto with real.
(* Goal: @eq R (Rmult (pow e (Init.Nat.add (Init.Nat.sub (Pos.to_nat n1) (Pos.to_nat m1)) (Pos.to_nat m1))) (Rinv (pow e (Pos.to_nat m1)))) (Rmult (Rinv (pow e (Pos.to_nat m1))) (pow e (Pos.to_nat n1))) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
rewrite plus_comm; rewrite le_plus_minus_r; auto with real.
(* Goal: le (Pos.to_nat m1) (Pos.to_nat n1) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
apply lt_le_weak.
(* Goal: lt (Pos.to_nat m1) (Pos.to_nat n1) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
change (nat_of_P n1 > nat_of_P m1) in |- *.
(* Goal: gt (Pos.to_nat n1) (Pos.to_nat m1) *)
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
apply nat_of_P_gt_Gt_compare_morphism; auto.
(* Goal: forall (p p0 : positive) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (pow e (Pos.to_nat (Pos.add p0 p)))) (Rmult (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p)))) *)
intros n1 m1; rewrite nat_of_P_plus_morphism; auto with real.
(* Goal: forall _ : not (@eq R e (IZR Z0)), @eq R (Rinv (pow e (Init.Nat.add (Pos.to_nat m1) (Pos.to_nat n1)))) (Rmult (Rinv (pow e (Pos.to_nat m1))) (Rinv (pow e (Pos.to_nat n1)))) *)
intros H'; rewrite pow_add; auto with real.
(* Goal: @eq R (Rinv (Rmult (pow e (Pos.to_nat m1)) (pow e (Pos.to_nat n1)))) (Rmult (Rinv (pow e (Pos.to_nat m1))) (Rinv (pow e (Pos.to_nat n1)))) *)
apply Rinv_mult_distr; auto.
(* Goal: not (@eq R (pow e (Pos.to_nat n1)) (IZR Z0)) *)
apply pow_NR0; auto.
(* Goal: not (@eq R (pow e (Pos.to_nat n1)) (IZR Z0)) *)
apply pow_NR0; auto.
Qed.
Hint Resolve powerRZ_O powerRZ_1 powerRZ_NOR powerRZ_add: real.
 
Theorem powerRZ_Zopp :
 forall (e : R) (z : Z), e <> 0%R -> powerRZ e (- z) = (/ powerRZ e z)%R.
(* Goal: forall e : R, @eq R (powerRZ e (Z.succ Z0)) e *)
intros e z H; case z; simpl in |- *; auto with real.
(* Goal: forall p : positive, @eq R (pow e (Pos.to_nat p)) (Rinv (Rinv (pow e (Pos.to_nat p)))) *)
intros p; apply sym_eq; apply Rinv_involutive.
(* Goal: not (@eq R (pow e (Pos.to_nat p)) (IZR Z0)) *)
apply pow_nonzero; auto.
Qed.
 
Theorem powerRZ_Zs :
 forall (e : R) (n : Z),
 e <> 0%R -> powerRZ e (Zsucc n) = (e * powerRZ e n)%R.
(* Goal: forall (e : R) (n : Z) (_ : not (@eq R e (IZR Z0))), @eq R (powerRZ e (Z.succ n)) (Rmult e (powerRZ e n)) *)
intros e n H'0.
(* Goal: @eq R (powerRZ e (Z.succ n)) (Rmult e (powerRZ e n)) *)
replace (Zsucc n) with (n + Zsucc 0)%Z.
(* Goal: @eq R (powerRZ e (Z.add n (Z.succ Z0))) (Rmult e (powerRZ e n)) *)
(* Goal: @eq Z (Z.add n (Z.succ Z0)) (Z.succ n) *)
rewrite powerRZ_add; auto.
(* Goal: @eq R (Rmult (powerRZ e n) (powerRZ e (Z.succ Z0))) (Rmult e (powerRZ e n)) *)
(* Goal: @eq Z (Z.add n (Z.succ Z0)) (Z.succ n) *)
rewrite powerRZ_1.
(* Goal: @eq R (Rmult (powerRZ e n) e) (Rmult e (powerRZ e n)) *)
(* Goal: @eq Z (Z.add n (Z.succ Z0)) (Z.succ n) *)
rewrite Rmult_comm; auto.
(* Goal: @eq Z (Z.add n (Z.succ Z0)) (Z.succ n) *)
auto with zarith.
Qed.
(* Conversion theorem between relative numbers and reals *)
 
Theorem Zpower_nat_Z_powerRZ :
 forall (n : Z) (m : nat),
 IZR (Zpower_nat n m) = powerRZ (IZR n) (Z_of_nat m).
(* Goal: forall e : R, @eq R (powerRZ e (Z.succ Z0)) e *)
intros n m; elim m; simpl in |- *; auto with real.
(* Goal: forall (n0 : nat) (_ : @eq R (IZR (Zpower_nat n n0)) (powerRZ (IZR n) (Z.of_nat n0))), @eq R (IZR (Z.mul n (Zpower_nat n n0))) (pow (IZR n) (Pos.to_nat (Pos.of_succ_nat n0))) *)
intros m1 H'; rewrite nat_of_P_o_P_of_succ_nat_eq_succ; simpl in |- *.
(* Goal: @eq R (IZR (Z.mul n (Zpower_nat n m1))) (Rmult (IZR n) (pow (IZR n) m1)) *)
replace (Zpower_nat n (S m1)) with (n * Zpower_nat n m1)%Z.
(* Goal: @eq R (IZR (Z.mul n (Zpower_nat n m1))) (Rmult (IZR n) (pow (IZR n) m1)) *)
(* Goal: @eq Z (Z.mul n (Zpower_nat n m1)) (Zpower_nat n (S m1)) *)
rewrite Rmult_IZR; auto with real.
(* Goal: @eq R (Rmult (IZR n) (IZR (Zpower_nat n m1))) (Rmult (IZR n) (pow (IZR n) m1)) *)
(* Goal: @eq Z (Z.mul n (Zpower_nat n m1)) (Zpower_nat n (S m1)) *)
rewrite H'; simpl in |- *.
(* Goal: forall e : R, @eq R (powerRZ e (Z.succ Z0)) e *)
case m1; simpl in |- *; auto with real.
(* Goal: forall n0 : nat, @eq R (Rmult (IZR n) (pow (IZR n) (Pos.to_nat (Pos.of_succ_nat n0)))) (Rmult (IZR n) (Rmult (IZR n) (pow (IZR n) n0))) *)
(* Goal: @eq Z (Z.mul n (Zpower_nat n m1)) (Zpower_nat n (S m1)) *)
intros m2; rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto.
(* Goal: @eq Z (Z.mul n (Zpower_nat n m1)) (Zpower_nat n (S m1)) *)
unfold Zpower_nat in |- *; auto.
Qed.
 
Theorem powerRZ_lt : forall (e : R) (z : Z), (0 < e)%R -> (0 < powerRZ e z)%R.
(* Goal: forall e : R, @eq R (powerRZ e (Z.succ Z0)) e *)
intros e z; case z; simpl in |- *; auto with real.
Qed.
Hint Resolve powerRZ_lt: real.
 
Theorem powerRZ_le :
 forall (e : R) (z : Z), (0 < e)%R -> (0 <= powerRZ e z)%R.
(* Goal: forall (e : R) (z : Z) (_ : Rlt (IZR Z0) e), Rle (IZR Z0) (powerRZ e z) *)
intros e z H'; apply Rlt_le; auto with real.
Qed.
Hint Resolve powerRZ_le: real.
 
Theorem Rlt_powerRZ :
 forall (e : R) (n m : Z),
 (1 < e)%R -> (n < m)%Z -> (powerRZ e n < powerRZ e m)%R.
intros e n m; case n; case m; simpl in |- *;
 try (unfold Zlt in |- *; intros; discriminate); auto with real.
(* Goal: forall (p p0 : positive) (_ : Rlt (IZR (Zpos xH)) e) (_ : Z.lt (Zpos p0) (Zpos p)), Rlt (pow e (Pos.to_nat p0)) (pow e (Pos.to_nat p)) *)
(* Goal: forall (p : positive) (_ : Rlt (IZR (Zpos xH)) e) (_ : Z.lt (Zneg p) Z0), Rlt (Rinv (pow e (Pos.to_nat p))) (IZR (Zpos xH)) *)
(* Goal: forall (p p0 : positive) (_ : Rlt (IZR (Zpos xH)) e) (_ : Z.lt (Zneg p0) (Zpos p)), Rlt (Rinv (pow e (Pos.to_nat p0))) (pow e (Pos.to_nat p)) *)
(* Goal: forall (p p0 : positive) (_ : Rlt (IZR (Zpos xH)) e) (_ : Z.lt (Zneg p0) (Zneg p)), Rlt (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p))) *)
intros p p0 H' H'0; apply Rlt_pow; auto with real.
(* Goal: lt (Pos.to_nat p0) (Pos.to_nat p) *)
(* Goal: forall (p : positive) (_ : Rlt (IZR (Zpos xH)) e) (_ : Z.lt (Zneg p) Z0), Rlt (Rinv (pow e (Pos.to_nat p))) (IZR (Zpos xH)) *)
(* Goal: forall (p p0 : positive) (_ : Rlt (IZR (Zpos xH)) e) (_ : Z.lt (Zneg p0) (Zpos p)), Rlt (Rinv (pow e (Pos.to_nat p0))) (pow e (Pos.to_nat p)) *)
(* Goal: forall (p p0 : positive) (_ : Rlt (IZR (Zpos xH)) e) (_ : Z.lt (Zneg p0) (Zneg p)), Rlt (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p))) *)
apply nat_of_P_lt_Lt_compare_morphism; auto.
(* Goal: forall (p : positive) (_ : Rlt (IZR (Zpos xH)) e) (_ : Z.lt (Zneg p) Z0), Rlt (Rinv (pow e (Pos.to_nat p))) (IZR (Zpos xH)) *)
(* Goal: forall (p p0 : positive) (_ : Rlt (IZR (Zpos xH)) e) (_ : Z.lt (Zneg p0) (Zpos p)), Rlt (Rinv (pow e (Pos.to_nat p0))) (pow e (Pos.to_nat p)) *)
(* Goal: forall (p p0 : positive) (_ : Rlt (IZR (Zpos xH)) e) (_ : Z.lt (Zneg p0) (Zneg p)), Rlt (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p))) *)
intros p H' H'0; replace 1%R with (/ 1)%R; auto with real.
(* Goal: forall (p p0 : positive) (_ : Rlt (IZR (Zpos xH)) e) (_ : Z.lt (Zneg p0) (Zpos p)), Rlt (Rinv (pow e (Pos.to_nat p0))) (pow e (Pos.to_nat p)) *)
(* Goal: forall (p p0 : positive) (_ : Rlt (IZR (Zpos xH)) e) (_ : Z.lt (Zneg p0) (Zneg p)), Rlt (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p))) *)
intros p p0 H' H'0; apply Rlt_trans with (r2 := 1%R).
(* Goal: Rlt (Rinv (pow e (Pos.to_nat p0))) (IZR (Zpos xH)) *)
(* Goal: Rlt (IZR (Zpos xH)) (pow e (Pos.to_nat p)) *)
(* Goal: forall (p p0 : positive) (_ : Rlt (IZR (Zpos xH)) e) (_ : Z.lt (Zneg p0) (Zneg p)), Rlt (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p))) *)
replace 1%R with (/ 1)%R; auto with real.
(* Goal: Rlt (IZR (Zpos xH)) (pow e (Pos.to_nat p)) *)
(* Goal: forall (p p0 : positive) (_ : Rlt (IZR (Zpos xH)) e) (_ : Z.lt (Zneg p0) (Zneg p)), Rlt (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p))) *)
apply Rlt_pow_R1; auto with real.
(* Goal: forall (p p0 : positive) (_ : Rlt (IZR (Zpos xH)) e) (_ : Z.lt (Zneg p0) (Zneg p)), Rlt (Rinv (pow e (Pos.to_nat p0))) (Rinv (pow e (Pos.to_nat p))) *)
intros p p0 H' H'0; apply Rinv_1_lt_contravar; auto with real.
(* Goal: Rlt (pow e (Pos.to_nat p)) (pow e (Pos.to_nat p0)) *)
apply Rlt_pow; auto with real.
(* Goal: lt (Pos.to_nat p) (Pos.to_nat p0) *)
apply nat_of_P_lt_Lt_compare_morphism; rewrite ZC4; auto.
Qed.
Hint Resolve Rlt_powerRZ: real.
 
Theorem Rpow_R1 :
 forall (r : R) (z : Z),
 r <> 0%R -> powerRZ r z = 1%R -> Rabs r = 1%R \/ z = 0%Z.
(* Goal: forall (r : R) (z : Z) (_ : not (@eq R r (IZR Z0))) (_ : @eq R (powerRZ r z) (IZR (Zpos xH))), or (@eq R (Rabs r) (IZR (Zpos xH))) (@eq Z z Z0) *)
intros r z; case z; simpl in |- *; auto; intros p H' H'1; left.
(* Goal: @eq R (Rabs r) (IZR (Zpos xH)) *)
case (pow_R1 _ _ H'1); auto.
(* Goal: forall _ : @eq nat (Pos.to_nat p) O, @eq R (Rabs r) (IZR (Zpos xH)) *)
intros H'0; Contradict H'0; auto with zarith; apply convert_not_O.
(* Goal: @eq R (Rabs r) (IZR (Zpos xH)) *)
rewrite Rinv_pow in H'1; auto.
(* Goal: @eq R (Rabs r) (IZR (Zpos xH)) *)
case (pow_R1 _ _ H'1); auto.
(* Goal: forall _ : @eq R (Rabs (Rinv r)) (IZR (Zpos xH)), @eq R (Rabs r) (IZR (Zpos xH)) *)
(* Goal: forall _ : @eq nat (Pos.to_nat p) O, @eq R (Rabs r) (IZR (Zpos xH)) *)
intros H'0.
(* Goal: @eq R (Rabs r) (IZR (Zpos xH)) *)
(* Goal: forall _ : @eq nat (Pos.to_nat p) O, @eq R (Rabs r) (IZR (Zpos xH)) *)
rewrite <- H'0.
(* Goal: @eq R (Rabs r) (Rabs (Rinv r)) *)
(* Goal: forall _ : @eq nat (Pos.to_nat p) O, @eq R (Rabs r) (IZR (Zpos xH)) *)
apply Rmult_eq_reg_l with (r := 1%R); auto with real.
(* Goal: @eq R (Rmult (IZR (Zpos xH)) (Rabs r)) (Rmult (IZR (Zpos xH)) (Rabs (Rinv r))) *)
(* Goal: forall _ : @eq nat (Pos.to_nat p) O, @eq R (Rabs r) (IZR (Zpos xH)) *)
pattern 1%R at 1 in |- *; rewrite <- H'0; auto with real.
pattern (Rabs (/ r)) at 1 in |- *; rewrite Rabs_Rinv; try rewrite Rinv_l;
 auto with real.
(* Goal: @eq R (IZR (Zpos xH)) (Rmult (IZR (Zpos xH)) (Rabs (Rinv r))) *)
(* Goal: not (@eq R (Rabs r) (IZR Z0)) *)
(* Goal: forall _ : @eq nat (Pos.to_nat p) O, @eq R (Rabs r) (IZR (Zpos xH)) *)
rewrite H'0; auto with real.
(* Goal: not (@eq R (Rabs r) (IZR Z0)) *)
(* Goal: forall _ : @eq nat (Pos.to_nat p) O, @eq R (Rabs r) (IZR (Zpos xH)) *)
apply Rabs_no_R0; auto.
(* Goal: forall _ : @eq nat (Pos.to_nat p) O, @eq R (Rabs r) (IZR (Zpos xH)) *)
intros H'0; Contradict H'0; auto with zarith; apply convert_not_O.
Qed.
 
Theorem Rpow_eq_inv :
 forall (r : R) (p q : Z),
 r <> 0%R -> Rabs r <> 1%R -> powerRZ r p = powerRZ r q -> p = q.
(* Goal: forall (r : R) (p q : Z) (_ : not (@eq R r (IZR Z0))) (_ : not (@eq R (Rabs r) (IZR (Zpos xH)))) (_ : @eq R (powerRZ r p) (powerRZ r q)), @eq Z p q *)
intros r p q H' H'0 H'1.
(* Goal: @eq Z p q *)
cut (powerRZ r (p - q) = 1%R); [ intros Eq0 | idtac ].
(* Goal: @eq Z (Z.add n (Z.succ Z0)) (Z.succ n) *)
case (Rpow_R1 _ _ H' Eq0); auto with zarith.
(* Goal: forall _ : @eq R (Rabs r) (IZR (Zpos xH)), @eq Z p q *)
(* Goal: @eq R (powerRZ r (Z.sub p q)) (IZR (Zpos xH)) *)
intros H'2; case H'0; auto.
(* Goal: @eq R (powerRZ r (Z.sub p q)) (IZR (Zpos xH)) *)
apply Rmult_eq_reg_l with (r := powerRZ r q); auto with real.
(* Goal: @eq R (Rmult (powerRZ r q) (powerRZ r (Z.sub p q))) (Rmult (powerRZ r q) (IZR (Zpos xH))) *)
rewrite <- powerRZ_add; auto.
(* Goal: @eq Z (Z.add n (Z.succ Z0)) (Z.succ n) *)
replace (q + (p - q))%Z with p; auto with zarith.
(* Goal: @eq R (powerRZ r p) (Rmult (powerRZ r q) (IZR (Zpos xH))) *)
rewrite <- H'1; rewrite Rmult_1_r; auto with arith.
Qed.
 
Theorem Zpower_nat_powerRZ_absolu :
 forall n m : Z,
 (0 <= m)%Z -> IZR (Zpower_nat n (Zabs_nat m)) = powerRZ (IZR n) m.
(* Goal: @eq Z (Z.add n (Z.succ Z0)) (Z.succ n) *)
intros n m; case m; simpl in |- *; auto with zarith.
(* Goal: @eq Z (Z.add n (Z.succ Z0)) (Z.succ n) *)
intros p H'; elim (nat_of_P p); simpl in |- *; auto with zarith.
(* Goal: @eq Z (Z.add n (Z.succ Z0)) (Z.succ n) *)
intros n0 H'0; rewrite <- H'0; simpl in |- *; auto with zarith.
(* Goal: @eq R (IZR (Z.mul n (Zpower_nat n n0))) (Rmult (IZR n) (IZR (Zpower_nat n n0))) *)
(* Goal: forall (p : positive) (_ : Z.le Z0 (Zneg p)), @eq R (IZR (Zpower_nat n (Pos.to_nat p))) (Rinv (pow (IZR n) (Pos.to_nat p))) *)
rewrite <- Rmult_IZR; auto.
(* Goal: @eq Z (Z.add n (Z.succ Z0)) (Z.succ n) *)
intros p H'; Contradict H'; auto with zarith.
Qed.
 
Theorem powerRZ_R1 : forall n : Z, powerRZ 1 n = 1%R.
(* Goal: forall e : R, @eq R (powerRZ e Z0) (IZR (Zpos xH)) *)
intros n; case n; simpl in |- *; auto.
intros p; elim (nat_of_P p); simpl in |- *; auto; intros n0 H'; rewrite H';
 ring.
(* Goal: forall p : positive, @eq R (Rinv (pow (IZR (Zpos xH)) (Pos.to_nat p))) (IZR (Zpos xH)) *)
intros p; elim (nat_of_P p); simpl in |- *.
(* Goal: @eq R (Rinv (IZR (Zpos xH))) (IZR (Zpos xH)) *)
(* Goal: forall (n : nat) (_ : @eq R (Rinv (pow (IZR (Zpos xH)) n)) (IZR (Zpos xH))), @eq R (Rinv (Rmult (IZR (Zpos xH)) (pow (IZR (Zpos xH)) n))) (IZR (Zpos xH)) *)
exact Rinv_1.
intros n1 H'; rewrite Rinv_mult_distr; try rewrite Rinv_1; try rewrite H';
 auto with real.
Qed.
 
Theorem Rle_powerRZ :
 forall (e : R) (n m : Z),
 (1 <= e)%R -> (n <= m)%Z -> (powerRZ e n <= powerRZ e m)%R.
(* Goal: forall (e : R) (n m : Z) (_ : Rlt (IZR (Zpos xH)) e) (_ : Rle (powerRZ e n) (powerRZ e m)), Z.le n m *)
intros e n m H' H'0.
(* Goal: Rle (powerRZ e n) (powerRZ e m) *)
case H'; intros E1.
(* Goal: Rle (powerRZ e n) (powerRZ e m) *)
(* Goal: Rle (powerRZ e n) (powerRZ e m) *)
case (Zle_lt_or_eq _ _ H'0); intros E2.
(* Goal: Rle (powerRZ e n) (powerRZ e m) *)
(* Goal: Rle (powerRZ e n) (powerRZ e m) *)
(* Goal: Rle (powerRZ e n) (powerRZ e m) *)
apply Rlt_le; auto with real.
(* Goal: Rle (powerRZ e n) (powerRZ e m) *)
(* Goal: Rle (powerRZ e n) (powerRZ e m) *)
rewrite <- E2; auto with real.
(* Goal: Rle (powerRZ e n) (powerRZ e m) *)
repeat rewrite <- E1; repeat rewrite powerRZ_R1; auto with real.
Qed.
 
Theorem Zlt_powerRZ :
 forall (e : R) (n m : Z),
 (1 <= e)%R -> (powerRZ e n < powerRZ e m)%R -> (n < m)%Z.
(* Goal: forall (e : R) (n m : Z) (_ : Rlt (IZR (Zpos xH)) e) (_ : Rle (powerRZ e n) (powerRZ e m)), Z.le n m *)
intros e n m H' H'0.
(* Goal: Z.lt n m *)
case (Zle_or_lt m n); auto; intros Z1.
(* Goal: Z.lt n m *)
Contradict H'0.
(* Goal: not (Rlt (powerRZ e n) (powerRZ e m)) *)
apply Rle_not_lt.
(* Goal: Rle (powerRZ e m) (powerRZ e n) *)
apply Rle_powerRZ; auto.
Qed.
 
Theorem Zle_powerRZ :
 forall (e : R) (n m : Z),
 (1 < e)%R -> (powerRZ e n <= powerRZ e m)%R -> (n <= m)%Z.
(* Goal: forall (e : R) (n m : Z) (_ : Rlt (IZR (Zpos xH)) e) (_ : Rle (powerRZ e n) (powerRZ e m)), Z.le n m *)
intros e n m H' H'0.
(* Goal: Z.le n m *)
case (Zle_or_lt n m); auto; intros Z1.
(* Goal: Z.le n m *)
absurd (powerRZ e n <= powerRZ e m)%R; auto.
(* Goal: not (Rle (powerRZ e n) (powerRZ e m)) *)
apply Rlt_not_le.
(* Goal: Rlt (powerRZ e m) (powerRZ e n) *)
apply Rlt_powerRZ; auto.
Qed.
 
Theorem Rinv_powerRZ :
 forall (e : R) (n : Z), e <> 0%R -> (/ powerRZ e n)%R = powerRZ e (- n).
(* Goal: forall (e : R) (n : Z) (_ : not (@eq R e (IZR Z0))), @eq R (Rinv (powerRZ e n)) (powerRZ e (Z.opp n)) *)
intros e n H.
(* Goal: @eq R (Rinv (powerRZ e n)) (powerRZ e (Z.opp n)) *)
apply Rmult_eq_reg_l with (powerRZ e n); auto with real zarith.
(* Goal: @eq R (Rmult (powerRZ e n) (Rinv (powerRZ e n))) (Rmult (powerRZ e n) (powerRZ e (Z.opp n))) *)
rewrite Rinv_r; auto with real zarith.
(* Goal: @eq R (IZR (Zpos xH)) (Rmult (powerRZ e n) (powerRZ e (Z.opp n))) *)
rewrite <- powerRZ_add; auto with real zarith.
(* Goal: forall e : R, @eq R (powerRZ e Z0) (IZR (Zpos xH)) *)
ring_simplify (n + - n)%Z; simpl in |- *; auto.
Qed.
