diff options
| -rw-r--r-- | theories/Reals/Rtrigo_def.v | 40 |
1 files changed, 13 insertions, 27 deletions
diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 9aed67657a..2004f40f00 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -41,8 +41,13 @@ Proof. red; intro; rewrite H0 in H; elim (lt_irrefl _ H). Qed. -Lemma exist_exp0 : exp_in 0 1. +(* Value of [exp 0] *) +Lemma exp_0 : exp 0 = 1. Proof. + cut (exp_in 0 1). + cut (exp_in 0 (exp 0)). + apply uniqueness_sum. + exact (proj2_sig (exist_exp 0)). unfold exp_in; unfold infinite_sum; intros. exists 0%nat. intros; replace (sum_f_R0 (fun i:nat => / INR (fact i) * 0 ^ i) n) with 1. @@ -57,18 +62,6 @@ Proof. unfold ge; apply le_O_n. Qed. -(* Value of [exp 0] *) -Lemma exp_0 : exp 0 = 1. -Proof. - cut (exp_in 0 (exp 0)). - cut (exp_in 0 1). - unfold exp_in; intros; eapply uniqueness_sum. - apply H0. - apply H. - exact exist_exp0. - exact (proj2_sig (exist_exp 0)). -Qed. - (*****************************************) (** * Definition of hyperbolic functions *) (*****************************************) @@ -383,8 +376,14 @@ Proof. intros; ring. Qed. -Lemma exist_cos0 : cos_in 0 1. +(* Value of [cos 0] *) +Lemma cos_0 : cos 0 = 1. Proof. + cut (cos_in 0 1). + cut (cos_in 0 (cos 0)). + apply uniqueness_sum. + rewrite <- Rsqr_0 at 1. + exact (proj2_sig (exist_cos (Rsqr 0))). unfold cos_in; unfold infinite_sum; intros; exists 0%nat. intros. unfold R_dist. @@ -399,16 +398,3 @@ Proof. apply Hrecn; unfold ge; apply le_O_n. simpl; ring. Qed. - -(* Value of [cos 0] *) -Lemma cos_0 : cos 0 = 1. -Proof. - cut (cos_in 0 (cos 0)). - cut (cos_in 0 1). - unfold cos_in; intros; eapply uniqueness_sum. - apply H0. - apply H. - exact exist_cos0. - assert (H := proj2_sig (exist_cos (Rsqr 0))); unfold cos; - pattern 0 at 1; replace 0 with (Rsqr 0); [ exact H | apply Rsqr_0 ]. -Qed. |