diff options
Diffstat (limited to 'theories/Reals/Rpower.v')
| -rw-r--r-- | theories/Reals/Rpower.v | 168 |
1 files changed, 84 insertions, 84 deletions
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index 593e54c6..43f326a0 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -15,25 +15,25 @@ Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. -Require Import Rtrigo. +Require Import Rtrigo1. Require Import Ranalysis1. Require Import Exp_prop. Require Import Rsqrt_def. Require Import R_sqrt. Require Import MVT. Require Import Ranalysis4. -Open Local Scope R_scope. +Local Open Scope R_scope. Lemma P_Rmin : forall (P:R -> Prop) (x y:R), P x -> P y -> P (Rmin x y). Proof. - intros P x y H1 H2; unfold Rmin in |- *; case (Rle_dec x y); intro; + intros P x y H1 H2; unfold Rmin; case (Rle_dec x y); intro; assumption. Qed. Lemma exp_le_3 : exp 1 <= 3. Proof. assert (exp_1 : exp 1 <> 0). - assert (H0 := exp_pos 1); red in |- *; intro; rewrite H in H0; + assert (H0 := exp_pos 1); red; intro; rewrite H in H0; elim (Rlt_irrefl _ H0). apply Rmult_le_reg_l with (/ exp 1). apply Rinv_0_lt_compat; apply exp_pos. @@ -43,7 +43,7 @@ Proof. rewrite Rmult_1_r; rewrite <- (Rmult_comm 3); rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. rewrite Rmult_1_l; replace (/ exp 1) with (exp (-1)). - unfold exp in |- *; case (exist_exp (-1)); intros; simpl in |- *; + unfold exp; case (exist_exp (-1)); intros; simpl; unfold exp_in in e; assert (H := alternated_series_ineq (fun i:nat => / INR (fact i)) x 1). cut @@ -73,7 +73,7 @@ Proof. ring. discrR. apply H. - unfold Un_decreasing in |- *; intros; + unfold Un_decreasing; intros; apply Rmult_le_reg_l with (INR (fact n)). apply INR_fact_lt_0. apply Rmult_le_reg_l with (INR (fact (S n))). @@ -84,13 +84,13 @@ Proof. rewrite Rmult_1_r; apply le_INR; apply fact_le; apply le_n_Sn. apply INR_fact_neq_0. apply INR_fact_neq_0. - assert (H0 := cv_speed_pow_fact 1); unfold Un_cv in |- *; unfold Un_cv in H0; + assert (H0 := cv_speed_pow_fact 1); unfold Un_cv; unfold Un_cv in H0; intros; elim (H0 _ H1); intros; exists x0; intros; - unfold R_dist in H2; unfold R_dist in |- *; + unfold R_dist in H2; unfold R_dist; replace (/ INR (fact n)) with (1 ^ n / INR (fact n)). apply (H2 _ H3). - unfold Rdiv in |- *; rewrite pow1; rewrite Rmult_1_l; reflexivity. - unfold infinite_sum in e; unfold Un_cv, tg_alt in |- *; intros; elim (e _ H0); + unfold Rdiv; rewrite pow1; rewrite Rmult_1_l; reflexivity. + unfold infinite_sum in e; unfold Un_cv, tg_alt; intros; elim (e _ H0); intros; exists x0; intros; replace (sum_f_R0 (fun i:nat => (-1) ^ i * / INR (fact i)) n) with (sum_f_R0 (fun i:nat => / INR (fact i) * (-1) ^ i) n). @@ -121,7 +121,7 @@ Proof. intro. replace (derive_pt exp x0 (H0 x0)) with (exp x0). apply exp_pos. - symmetry in |- *; apply derive_pt_eq_0. + symmetry ; apply derive_pt_eq_0. apply (derivable_pt_lim_exp x0). apply H. Qed. @@ -143,11 +143,11 @@ Proof. rewrite Ropp_0; rewrite Rplus_0_r; replace (derive_pt exp x0 (derivable_exp x0)) with (exp x0). rewrite exp_0; rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l; - pattern x at 1 in |- *; rewrite <- Rmult_1_r; rewrite (Rmult_comm (exp x0)); + pattern x at 1; rewrite <- Rmult_1_r; rewrite (Rmult_comm (exp x0)); apply Rmult_lt_compat_l. apply H. rewrite <- exp_0; apply exp_increasing; elim H3; intros; assumption. - symmetry in |- *; apply derive_pt_eq_0; apply derivable_pt_lim_exp. + symmetry ; apply derive_pt_eq_0; apply derivable_pt_lim_exp. Qed. Lemma ln_exists1 : forall y:R, 1 <= y -> { z:R | y = exp z }. @@ -160,18 +160,18 @@ Proof. cut (f 0 * f y <= 0); [intro H4|]. pose proof (IVT_cor f 0 y H2 (Rlt_le _ _ H0) H4) as (t,(_,H7)); exists t; unfold f in H7; apply Rminus_diag_uniq_sym; exact H7. - pattern 0 at 2 in |- *; rewrite <- (Rmult_0_r (f y)); + pattern 0 at 2; rewrite <- (Rmult_0_r (f y)); rewrite (Rmult_comm (f 0)); apply Rmult_le_compat_l; assumption. - unfold f in |- *; apply Rplus_le_reg_l with y; left; + unfold f; apply Rplus_le_reg_l with y; left; apply Rlt_trans with (1 + y). rewrite <- (Rplus_comm y); apply Rplus_lt_compat_l; apply Rlt_0_1. replace (y + (exp y - y)) with (exp y); [ apply (exp_ineq1 y H0) | ring ]. - unfold f in |- *; change (continuity (exp - fct_cte y)) in |- *; + unfold f; change (continuity (exp - fct_cte y)); apply continuity_minus; [ apply derivable_continuous; apply derivable_exp | apply derivable_continuous; apply derivable_const ]. - unfold f in |- *; rewrite exp_0; apply Rplus_le_reg_l with y; + unfold f; rewrite exp_0; apply Rplus_le_reg_l with y; rewrite Rplus_0_r; replace (y + (1 - y)) with 1; [ apply H | ring ]. Qed. @@ -185,18 +185,18 @@ Proof. apply H. rewrite <- Rinv_r_sym. rewrite Rmult_1_r; left; apply (Rnot_le_lt _ _ n). - red in |- *; intro; rewrite H0 in H; elim (Rlt_irrefl _ H). + red; intro; rewrite H0 in H; elim (Rlt_irrefl _ H). destruct (ln_exists1 _ H0) as (x,p); exists (- x); apply Rmult_eq_reg_l with (exp x / y). - unfold Rdiv in |- *; rewrite Rmult_assoc; rewrite <- Rinv_l_sym. + unfold Rdiv; rewrite Rmult_assoc; rewrite <- Rinv_l_sym. rewrite Rmult_1_r; rewrite <- (Rmult_comm (/ y)); rewrite Rmult_assoc; rewrite <- exp_plus; rewrite Rplus_opp_r; rewrite exp_0; - rewrite Rmult_1_r; symmetry in |- *; apply p. - red in |- *; intro H3; rewrite H3 in H; elim (Rlt_irrefl _ H). - unfold Rdiv in |- *; apply prod_neq_R0. - assert (H3 := exp_pos x); red in |- *; intro H4; rewrite H4 in H3; + rewrite Rmult_1_r; symmetry ; apply p. + red; intro H3; rewrite H3 in H; elim (Rlt_irrefl _ H). + unfold Rdiv; apply prod_neq_R0. + assert (H3 := exp_pos x); red; intro H4; rewrite H4 in H3; elim (Rlt_irrefl _ H3). - apply Rinv_neq_0_compat; red in |- *; intro H3; rewrite H3 in H; + apply Rinv_neq_0_compat; red; intro H3; rewrite H3 in H; elim (Rlt_irrefl _ H). Qed. @@ -213,11 +213,11 @@ Definition ln (x:R) : R := Lemma exp_ln : forall x:R, 0 < x -> exp (ln x) = x. Proof. - intros; unfold ln in |- *; case (Rlt_dec 0 x); intro. - unfold Rln in |- *; + intros; unfold ln; case (Rlt_dec 0 x); intro. + unfold Rln; case (ln_exists (mkposreal x r) (cond_pos (mkposreal x r))); intros. - simpl in e; symmetry in |- *; apply e. + simpl in e; symmetry ; apply e. elim n; apply H. Qed. @@ -231,7 +231,7 @@ Qed. Theorem exp_Ropp : forall x:R, exp (- x) = / exp x. Proof. intros x; assert (H : exp x <> 0). - assert (H := exp_pos x); red in |- *; intro; rewrite H0 in H; + assert (H := exp_pos x); red; intro; rewrite H0 in H; elim (Rlt_irrefl _ H). apply Rmult_eq_reg_l with (r := exp x). rewrite <- exp_plus; rewrite Rplus_opp_r; rewrite exp_0. @@ -306,11 +306,11 @@ Theorem ln_continue : forall y:R, 0 < y -> continue_in ln (fun x:R => 0 < x) y. Proof. intros y H. - unfold continue_in, limit1_in, limit_in in |- *; intros eps Heps. + unfold continue_in, limit1_in, limit_in; intros eps Heps. cut (1 < exp eps); [ intros H1 | idtac ]. cut (exp (- eps) < 1); [ intros H2 | idtac ]. exists (Rmin (y * (exp eps - 1)) (y * (1 - exp (- eps)))); split. - red in |- *; apply P_Rmin. + red; apply P_Rmin. apply Rmult_lt_0_compat. assumption. apply Rplus_lt_reg_r with 1. @@ -321,7 +321,7 @@ Proof. apply Rplus_lt_reg_r with (exp (- eps)). rewrite Rplus_0_r; replace (exp (- eps) + (1 - exp (- eps))) with 1; [ apply H2 | ring ]. - unfold dist, R_met, R_dist in |- *; simpl in |- *. + unfold dist, R_met, R_dist; simpl. intros x [[H3 H4] H5]. cut (y * (x * / y) = x). intro Hxyy. @@ -351,7 +351,7 @@ Proof. rewrite Hxyy; rewrite Rmult_1_r; apply Hxy. rewrite Hxy; rewrite Rinv_r. rewrite ln_1; rewrite Rabs_R0; apply Heps. - red in |- *; intro; rewrite H0 in H; elim (Rlt_irrefl _ H). + red; intro; rewrite H0 in H; elim (Rlt_irrefl _ H). rewrite Rabs_right. apply exp_lt_inv. rewrite exp_ln. @@ -366,7 +366,7 @@ Proof. left; apply (Rgt_minus _ _ Hxy). apply Rmult_lt_0_compat; [ apply H3 | apply (Rinv_0_lt_compat _ H) ]. rewrite <- ln_1. - apply Rgt_ge; red in |- *; apply ln_increasing. + apply Rgt_ge; red; apply ln_increasing. apply Rlt_0_1. apply Rmult_lt_reg_l with (r := y). apply H. @@ -379,7 +379,7 @@ Proof. apply Rinv_0_lt_compat; assumption. rewrite (Rmult_comm x); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym. ring. - red in |- *; intro; rewrite H0 in H; elim (Rlt_irrefl _ H). + red; intro; rewrite H0 in H; elim (Rlt_irrefl _ H). apply Rmult_lt_reg_l with (exp eps). apply exp_pos. rewrite <- exp_plus; rewrite Rmult_1_r; rewrite Rplus_opp_r; rewrite exp_0; @@ -394,7 +394,7 @@ Qed. Definition Rpower (x y:R) := exp (y * ln x). -Infix Local "^R" := Rpower (at level 30, right associativity) : R_scope. +Local Infix "^R" := Rpower (at level 30, right associativity) : R_scope. (******************************************************************) (** * Properties of Rpower *) @@ -412,13 +412,13 @@ Infix Local "^R" := Rpower (at level 30, right associativity) : R_scope. Theorem Rpower_plus : forall x y z:R, z ^R (x + y) = z ^R x * z ^R y. Proof. - intros x y z; unfold Rpower in |- *. + intros x y z; unfold Rpower. rewrite Rmult_plus_distr_r; rewrite exp_plus; auto. Qed. Theorem Rpower_mult : forall x y z:R, (x ^R y) ^R z = x ^R (y * z). Proof. - intros x y z; unfold Rpower in |- *. + intros x y z; unfold Rpower. rewrite ln_exp. replace (z * (y * ln x)) with (y * z * ln x). reflexivity. @@ -427,22 +427,22 @@ Qed. Theorem Rpower_O : forall x:R, 0 < x -> x ^R 0 = 1. Proof. - intros x _; unfold Rpower in |- *. + intros x _; unfold Rpower. rewrite Rmult_0_l; apply exp_0. Qed. Theorem Rpower_1 : forall x:R, 0 < x -> x ^R 1 = x. Proof. - intros x H; unfold Rpower in |- *. + intros x H; unfold Rpower. rewrite Rmult_1_l; apply exp_ln; apply H. Qed. Theorem Rpower_pow : forall (n:nat) (x:R), 0 < x -> x ^R INR n = x ^ n. Proof. - intros n; elim n; simpl in |- *; auto; fold INR in |- *. + intros n; elim n; simpl; auto; fold INR. intros x H; apply Rpower_O; auto. intros n1; case n1. - intros H x H0; simpl in |- *; rewrite Rmult_1_r; apply Rpower_1; auto. + intros H x H0; simpl; rewrite Rmult_1_r; apply Rpower_1; auto. intros n0 H x H0; rewrite Rpower_plus; rewrite H; try rewrite Rpower_1; try apply Rmult_comm || assumption. Qed. @@ -451,7 +451,7 @@ Theorem Rpower_lt : forall x y z:R, 1 < x -> 0 <= y -> y < z -> x ^R y < x ^R z. Proof. intros x y z H H0 H1. - unfold Rpower in |- *. + unfold Rpower. apply exp_increasing. apply Rmult_lt_compat_r. rewrite <- ln_1; apply ln_increasing. @@ -464,18 +464,18 @@ Theorem Rpower_sqrt : forall x:R, 0 < x -> x ^R (/ 2) = sqrt x. Proof. intros x H. apply ln_inv. - unfold Rpower in |- *; apply exp_pos. + unfold Rpower; apply exp_pos. apply sqrt_lt_R0; apply H. apply Rmult_eq_reg_l with (INR 2). apply exp_inv. - fold Rpower in |- *. + fold Rpower. cut ((x ^R (/ INR 2)) ^R INR 2 = sqrt x ^R INR 2). - unfold Rpower in |- *; auto. + unfold Rpower; auto. rewrite Rpower_mult. rewrite Rinv_l. replace 1 with (INR 1); auto. - repeat rewrite Rpower_pow; simpl in |- *. - pattern x at 1 in |- *; rewrite <- (sqrt_sqrt x (Rlt_le _ _ H)). + repeat rewrite Rpower_pow; simpl. + pattern x at 1; rewrite <- (sqrt_sqrt x (Rlt_le _ _ H)). ring. apply sqrt_lt_R0; apply H. apply H. @@ -485,7 +485,7 @@ Qed. Theorem Rpower_Ropp : forall x y:R, x ^R (- y) = / x ^R y. Proof. - unfold Rpower in |- *. + unfold Rpower. intros x y; rewrite Ropp_mult_distr_l_reverse. apply exp_Ropp. Qed. @@ -505,11 +505,11 @@ Proof. rewrite Rinv_r. apply exp_lt_inv. apply Rle_lt_trans with (1 := exp_le_3). - change (3 < 2 ^R 2) in |- *. + change (3 < 2 ^R 2). repeat rewrite Rpower_plus; repeat rewrite Rpower_1. repeat rewrite Rmult_plus_distr_r; repeat rewrite Rmult_plus_distr_l; repeat rewrite Rmult_1_l. - pattern 3 at 1 in |- *; rewrite <- Rplus_0_r; replace (2 + 2) with (3 + 1); + pattern 3 at 1; rewrite <- Rplus_0_r; replace (2 + 2) with (3 + 1); [ apply Rplus_lt_compat_l; apply Rlt_0_1 | ring ]. prove_sup0. discrR. @@ -523,7 +523,7 @@ Theorem limit1_ext : forall (f g:R -> R) (D:R -> Prop) (l x:R), (forall x:R, D x -> f x = g x) -> limit1_in f D l x -> limit1_in g D l x. Proof. - intros f g D l x H; unfold limit1_in, limit_in in |- *. + intros f g D l x H; unfold limit1_in, limit_in. intros H0 eps H1; case (H0 eps); auto. intros x0 [H2 H3]; exists x0; split; auto. intros x1 [H4 H5]; rewrite <- H; auto. @@ -533,7 +533,7 @@ Theorem limit1_imp : forall (f:R -> R) (D D1:R -> Prop) (l x:R), (forall x:R, D1 x -> D x) -> limit1_in f D l x -> limit1_in f D1 l x. Proof. - intros f D D1 l x H; unfold limit1_in, limit_in in |- *. + intros f D D1 l x H; unfold limit1_in, limit_in. intros H0 eps H1; case (H0 eps H1); auto. intros alpha [H2 H3]; exists alpha; split; auto. intros d [H4 H5]; apply H3; split; auto. @@ -541,7 +541,7 @@ Qed. Theorem Rinv_Rdiv : forall x y:R, x <> 0 -> y <> 0 -> / (x / y) = y / x. Proof. - intros x y H1 H2; unfold Rdiv in |- *; rewrite Rinv_mult_distr. + intros x y H1 H2; unfold Rdiv; rewrite Rinv_mult_distr. rewrite Rinv_involutive. apply Rmult_comm. assumption. @@ -551,18 +551,18 @@ Qed. Theorem Dln : forall y:R, 0 < y -> D_in ln Rinv (fun x:R => 0 < x) y. Proof. - intros y Hy; unfold D_in in |- *. + intros y Hy; unfold D_in. apply limit1_ext with (f := fun x:R => / ((exp (ln x) - exp (ln y)) / (ln x - ln y))). intros x [HD1 HD2]; repeat rewrite exp_ln. - unfold Rdiv in |- *; rewrite Rinv_mult_distr. + unfold Rdiv; rewrite Rinv_mult_distr. rewrite Rinv_involutive. apply Rmult_comm. apply Rminus_eq_contra. - red in |- *; intros H2; case HD2. - symmetry in |- *; apply (ln_inv _ _ HD1 Hy H2). - apply Rminus_eq_contra; apply (sym_not_eq HD2). - apply Rinv_neq_0_compat; apply Rminus_eq_contra; red in |- *; intros H2; + red; intros H2; case HD2. + symmetry ; apply (ln_inv _ _ HD1 Hy H2). + apply Rminus_eq_contra; apply (not_eq_sym HD2). + apply Rinv_neq_0_compat; apply Rminus_eq_contra; red; intros H2; case HD2; apply ln_inv; auto. assumption. assumption. @@ -574,62 +574,62 @@ Proof. intros x [H1 H2]; split. split; auto. split; auto. - red in |- *; intros H3; case H2; apply ln_inv; auto. + red; intros H3; case H2; apply ln_inv; auto. apply limit_comp with (l := ln y) (g := fun x:R => (exp x - exp (ln y)) / (x - ln y)) (f := ln). apply ln_continue; auto. assert (H0 := derivable_pt_lim_exp (ln y)); unfold derivable_pt_lim in H0; - unfold limit1_in in |- *; unfold limit_in in |- *; - simpl in |- *; unfold R_dist in |- *; intros; elim (H0 _ H); + unfold limit1_in; unfold limit_in; + simpl; unfold R_dist; intros; elim (H0 _ H); intros; exists (pos x); split. apply (cond_pos x). - intros; pattern y at 3 in |- *; rewrite <- exp_ln. - pattern x0 at 1 in |- *; replace x0 with (ln y + (x0 - ln y)); + intros; pattern y at 3; rewrite <- exp_ln. + pattern x0 at 1; replace x0 with (ln y + (x0 - ln y)); [ idtac | ring ]. apply H1. elim H2; intros H3 _; unfold D_x in H3; elim H3; clear H3; intros _ H3; - apply Rminus_eq_contra; apply (sym_not_eq (A:=R)); + apply Rminus_eq_contra; apply (not_eq_sym (A:=R)); apply H3. elim H2; clear H2; intros _ H2; apply H2. assumption. - red in |- *; intro; rewrite H in Hy; elim (Rlt_irrefl _ Hy). + red; intro; rewrite H in Hy; elim (Rlt_irrefl _ Hy). Qed. Lemma derivable_pt_lim_ln : forall x:R, 0 < x -> derivable_pt_lim ln x (/ x). Proof. intros; assert (H0 := Dln x H); unfold D_in in H0; unfold limit1_in in H0; unfold limit_in in H0; simpl in H0; unfold R_dist in H0; - unfold derivable_pt_lim in |- *; intros; elim (H0 _ H1); + unfold derivable_pt_lim; intros; elim (H0 _ H1); intros; elim H2; clear H2; intros; set (alp := Rmin x0 (x / 2)); assert (H4 : 0 < alp). - unfold alp in |- *; unfold Rmin in |- *; case (Rle_dec x0 (x / 2)); intro. + unfold alp; unfold Rmin; case (Rle_dec x0 (x / 2)); intro. apply H2. - unfold Rdiv in |- *; apply Rmult_lt_0_compat; + unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. - exists (mkposreal _ H4); intros; pattern h at 2 in |- *; + exists (mkposreal _ H4); intros; pattern h at 2; replace h with (x + h - x); [ idtac | ring ]. apply H3; split. - unfold D_x in |- *; split. + unfold D_x; split. case (Rcase_abs h); intro. assert (H7 : Rabs h < x / 2). apply Rlt_le_trans with alp. apply H6. - unfold alp in |- *; apply Rmin_r. + unfold alp; apply Rmin_r. apply Rlt_trans with (x / 2). - unfold Rdiv in |- *; apply Rmult_lt_0_compat; + unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. rewrite Rabs_left in H7. apply Rplus_lt_reg_r with (- h - x / 2). replace (- h - x / 2 + x / 2) with (- h); [ idtac | ring ]. - pattern x at 2 in |- *; rewrite double_var. + pattern x at 2; rewrite double_var. replace (- h - x / 2 + (x / 2 + x / 2 + h)) with (x / 2); [ apply H7 | ring ]. apply r. apply Rplus_lt_le_0_compat; [ assumption | apply Rge_le; apply r ]. - apply (sym_not_eq (A:=R)); apply Rminus_not_eq; replace (x + h - x) with h; + apply (not_eq_sym (A:=R)); apply Rminus_not_eq; replace (x + h - x) with h; [ apply H5 | ring ]. replace (x + h - x) with h; [ apply Rlt_le_trans with alp; - [ apply H6 | unfold alp in |- *; apply Rmin_l ] + [ apply H6 | unfold alp; apply Rmin_l ] | ring ]. Qed. @@ -637,7 +637,7 @@ Theorem D_in_imp : forall (f g:R -> R) (D D1:R -> Prop) (x:R), (forall x:R, D1 x -> D x) -> D_in f g D x -> D_in f g D1 x. Proof. - intros f g D D1 x H; unfold D_in in |- *. + intros f g D D1 x H; unfold D_in. intros H0; apply limit1_imp with (D := D_x D x); auto. intros x1 [H1 H2]; split; auto. Qed. @@ -646,7 +646,7 @@ Theorem D_in_ext : forall (f g h:R -> R) (D:R -> Prop) (x:R), f x = g x -> D_in h f D x -> D_in h g D x. Proof. - intros f g h D x H; unfold D_in in |- *. + intros f g h D x H; unfold D_in. rewrite H; auto. Qed. @@ -661,7 +661,7 @@ Proof. intros x H0; repeat split. assumption. apply D_in_ext with (f := fun x:R => / x * (z * exp (z * ln x))). - unfold Rminus in |- *; rewrite Rpower_plus; rewrite Rpower_Ropp; + unfold Rminus; rewrite Rpower_plus; rewrite Rpower_Ropp; rewrite (Rpower_1 _ H); unfold Rpower; ring. apply Dcomp with (f := ln) @@ -674,7 +674,7 @@ Proof. intros x H1; repeat split; auto. apply (Dcomp (fun _:R => True) (fun _:R => True) (fun x => z) exp - (fun x:R => z * x) exp); simpl in |- *. + (fun x:R => z * x) exp); simpl. apply D_in_ext with (f := fun x:R => z * 1). apply Rmult_1_r. apply (Dmult_const (fun x => True) (fun x => x) (fun x => 1)); apply Dx. @@ -687,16 +687,16 @@ Theorem derivable_pt_lim_power : 0 < x -> derivable_pt_lim (fun x => x ^R y) x (y * x ^R (y - 1)). Proof. intros x y H. - unfold Rminus in |- *; rewrite Rpower_plus. + unfold Rminus; rewrite Rpower_plus. rewrite Rpower_Ropp. rewrite Rpower_1; auto. rewrite <- Rmult_assoc. - unfold Rpower in |- *. + unfold Rpower. apply derivable_pt_lim_comp with (f1 := ln) (f2 := fun x => exp (y * x)). apply derivable_pt_lim_ln; assumption. rewrite (Rmult_comm y). apply derivable_pt_lim_comp with (f1 := fun x => y * x) (f2 := exp). - pattern y at 2 in |- *; replace y with (0 * ln x + y * 1). + pattern y at 2; replace y with (0 * ln x + y * 1). apply derivable_pt_lim_mult with (f1 := fun x:R => y) (f2 := fun x:R => x). apply derivable_pt_lim_const with (a := y). apply derivable_pt_lim_id. |