diff options
Diffstat (limited to 'theories/Reals/Exp_prop.v')
-rw-r--r-- | theories/Reals/Exp_prop.v | 24 |
1 files changed, 11 insertions, 13 deletions
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index dbf48e61a..160f3d480 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -723,15 +723,14 @@ Qed. (**********) Lemma exp_pos : forall x:R, 0 < exp x. Proof. - intro; case (total_order_T 0 x); intro. - elim s; intro. - apply (exp_pos_pos _ a). - rewrite <- b; rewrite exp_0; apply Rlt_0_1. + intro; destruct (total_order_T 0 x) as [[Hlt|<-]|Hgt]. + apply (exp_pos_pos _ Hlt). + rewrite exp_0; apply Rlt_0_1. replace (exp x) with (1 / exp (- x)). unfold Rdiv; apply Rmult_lt_0_compat. apply Rlt_0_1. apply Rinv_0_lt_compat; apply exp_pos_pos. - apply (Ropp_0_gt_lt_contravar _ r). + apply (Ropp_0_gt_lt_contravar _ Hgt). cut (exp (- x) <> 0). intro; unfold Rdiv; apply Rmult_eq_reg_l with (exp (- x)). rewrite Rmult_1_l; rewrite <- Rinv_r_sym. @@ -772,10 +771,10 @@ Proof. apply (not_eq_sym H6). rewrite Rminus_0_r; apply H7. unfold SFL. - case (cv 0); intros. + case (cv 0) as (x,Hu). eapply UL_sequence. - apply u. - unfold Un_cv, SP. + apply Hu. + unfold Un_cv, SP in |- *. intros; exists 1%nat; intros. unfold R_dist; rewrite decomp_sum. rewrite (Rplus_comm (fn 0%nat 0)). @@ -792,14 +791,13 @@ Proof. unfold Rdiv; rewrite Rinv_1; rewrite Rmult_1_r; reflexivity. apply lt_le_trans with 1%nat; [ apply lt_n_Sn | apply H9 ]. unfold SFL, exp. - case (cv h); case (exist_exp h); simpl; intros. + case (cv h) as (x0,Hu); case (exist_exp h) as (x,Hexp); simpl. eapply UL_sequence. - apply u. + apply Hu. unfold Un_cv; intros. - unfold exp_in in e. - unfold infinite_sum in e. + unfold exp_in, infinite_sum in Hexp. cut (0 < eps0 * Rabs h). - intro; elim (e _ H9); intros N0 H10. + intro; elim (Hexp _ H9); intros N0 H10. exists N0; intros. unfold R_dist. apply Rmult_lt_reg_l with (Rabs h). |