From 19752f81e096daac43119a144f8065dabbdb1e82 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 19 Feb 2021 19:05:35 +0100
Subject: Make intermediate lemmas more explicit, so that they can be
 terminated by Qed.

---
 theories/Reals/Rtrigo_def.v | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

(limited to 'theories')

diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v
index 7f5a859c81..9aed67657a 100644
--- a/theories/Reals/Rtrigo_def.v
+++ b/theories/Reals/Rtrigo_def.v
@@ -41,9 +41,8 @@ Proof.
   red; intro; rewrite H0 in H; elim (lt_irrefl _ H).
 Qed.
 
-Lemma exist_exp0 : { l:R | exp_in 0 l }.
+Lemma exist_exp0 : exp_in 0 1.
 Proof.
-  exists 1.
   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.
@@ -56,7 +55,7 @@ Proof.
   simpl.
   ring.
   unfold ge; apply le_O_n.
-Defined.
+Qed.
 
 (* Value of [exp 0] *)
 Lemma exp_0 : exp 0 = 1.
@@ -66,7 +65,7 @@ Proof.
   unfold exp_in; intros; eapply uniqueness_sum.
   apply H0.
   apply H.
-  exact (proj2_sig exist_exp0).
+  exact exist_exp0.
   exact (proj2_sig (exist_exp 0)).
 Qed.
 
@@ -384,9 +383,8 @@ Proof.
   intros; ring.
 Qed.
 
-Lemma exist_cos0 : { l:R | cos_in 0 l }.
+Lemma exist_cos0 : cos_in 0 1.
 Proof.
-  exists 1.
   unfold cos_in; unfold infinite_sum; intros; exists 0%nat.
   intros.
   unfold R_dist.
@@ -400,7 +398,7 @@ Proof.
   rewrite Rplus_0_r.
   apply Hrecn; unfold ge; apply le_O_n.
   simpl; ring.
-Defined.
+Qed.
 
 (* Value of [cos 0] *)
 Lemma cos_0 : cos 0 = 1.
@@ -410,7 +408,7 @@ Proof.
   unfold cos_in; intros; eapply uniqueness_sum.
   apply H0.
   apply H.
-  exact (proj2_sig exist_cos0).
+  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.
-- 
cgit v1.2.3