diff options
| author | Guillaume Melquiond | 2021-02-19 19:10:25 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2021-02-19 19:10:25 +0100 |
| commit | 88e688182ded232f474102d400e4e4e95861f94d (patch) | |
| tree | 59fa054515064ef255976f7df34b98621ea936b5 /theories | |
| parent | 19752f81e096daac43119a144f8065dabbdb1e82 (diff) | |
Terminate intermediate lemmas with Qed.
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Reals/Alembert.v | 8 | ||||
| -rw-r--r-- | theories/Reals/NewtonInt.v | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index 069a1292cd..9a00408de3 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -112,7 +112,7 @@ Proof. pattern (sum_f_R0 An n) at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left; apply H | apply H1 ]. -Defined. +Qed. Lemma Alembert_C2 : forall An:nat -> R, @@ -330,7 +330,7 @@ Proof. rewrite <- Rabs_Ropp; apply RRle_abs. rewrite double; pattern (Rabs (An n)) at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; apply Rabs_pos_lt; apply H. -Defined. +Qed. Lemma AlembertC3_step1 : forall (An:nat -> R) (x:R), @@ -374,7 +374,7 @@ Proof. [ assumption | apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption ]. intro; unfold Bn; apply prod_neq_R0; [ apply H0 | apply pow_nonzero; assumption ]. -Defined. +Qed. Lemma AlembertC3_step2 : forall (An:nat -> R) (x:R), x = 0 -> { l:R | Pser An x l }. @@ -405,7 +405,7 @@ Proof. cut (x <> 0). intro; apply AlembertC3_step1; assumption. red; intro; rewrite H1 in Hgt; elim (Rlt_irrefl _ Hgt). -Defined. +Qed. Lemma Alembert_C4 : forall (An:nat -> R) (k:R), diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v index 6692119738..6107775003 100644 --- a/theories/Reals/NewtonInt.v +++ b/theories/Reals/NewtonInt.v @@ -170,7 +170,7 @@ Proof. reg. exists H5; symmetry ; reg; rewrite <- H3; rewrite <- H4; reflexivity. assumption. -Defined. +Qed. (**********) Lemma antiderivative_P1 : |