Inline proofs of exist_exp0 and exist_cos0.

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.