diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-09-17 17:55:32 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-09-17 17:55:32 +0200 |
| commit | cc6afad3bcfaa5b7fa57c8cd3035fe520c93afda (patch) | |
| tree | 7b80f304b6a5bd6987b425e85e72055f3eb9d32b /theories/Reals | |
| parent | 95c915ce89cc168ec34ab36797c78de94fcc0a18 (diff) | |
Change some Defined into Qed.
Diffstat (limited to 'theories/Reals')
| -rw-r--r-- | theories/Reals/NewtonInt.v | 8 | ||||
| -rw-r--r-- | theories/Reals/Rtrigo_def.v | 2 |
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. |