aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--theories/Reals/NewtonInt.v8
-rw-r--r--theories/Reals/Rtrigo_def.v2
2 files changed, 6 insertions, 4 deletions
diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v
index e0bb8ee2b..82bd017a9 100644
--- a/theories/Reals/NewtonInt.v
+++ b/theories/Reals/NewtonInt.v
@@ -63,14 +63,16 @@ Proof.
[ apply derivable_pt_lim_const | apply derivable_pt_lim_id ]
| unfold id, fct_cte; rewrite H2; ring ].
right; reflexivity.
-Defined.
+Qed.
(* $\int_a^a f = 0$ *)
Lemma NewtonInt_P2 :
forall (f:R -> R) (a:R), NewtonInt f a a (NewtonInt_P1 f a) = 0.
Proof.
intros; unfold NewtonInt; simpl;
- unfold mult_fct, fct_cte, id; ring.
+ unfold mult_fct, fct_cte, id.
+ destruct NewtonInt_P1 as [g _].
+ now apply Rminus_diag_eq.
Qed.
(* If $\int_a^b f$ exists, then $\int_b^a f$ exists too *)
@@ -545,7 +547,7 @@ Proof.
assert (X2 := NewtonInt_P3 f b c X0).
apply NewtonInt_P3.
apply NewtonInt_P7 with b; assumption.
-Defined.
+Qed.
(* Chasles' relation *)
Lemma NewtonInt_P9 :
diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v
index 76d52efaa..95dcc3d72 100644
--- a/theories/Reals/Rtrigo_def.v
+++ b/theories/Reals/Rtrigo_def.v
@@ -340,7 +340,7 @@ Proof.
apply INR_eq; repeat rewrite S_INR; rewrite plus_INR; repeat rewrite mult_INR;
rewrite plus_INR; rewrite mult_INR; repeat rewrite S_INR;
replace (INR 0) with 0; [ ring | reflexivity ].
-Defined.
+Qed.
Lemma sin_no_R0 : forall n:nat, sin_n n <> 0.
Proof.