diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-06-21 15:27:31 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-06-21 15:27:31 +0000 |
| commit | 5ba4b0e3733bcb804d574f2123d01f3f4e5737e8 (patch) | |
| tree | e77c26e28d39965335b95dd600ac3c4606ac9d2a /theories/Reals/Alembert.v | |
| parent | 660d849297b98a6360f01ef029b7aa254e9e0b0b (diff) | |
Suppression de l'axiome d'extensionnalite
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2803 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Alembert.v')
| -rw-r--r-- | theories/Reals/Alembert.v | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index f1ed4cc69..10ebfc0c5 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -16,26 +16,22 @@ Require Rbase. Require Rseries. Require Rtrigo_fun. -Axiom fct_eq : (A:Type)(f1,f2:A->R) ((x:A)(f1 x)==(f2 x)) -> f1 == f2. - -Definition SigT := Specif.sigT. +(*********************) +(* Lemmes techniques *) +(*********************) Lemma not_sym : (r1,r2:R) ``r1<>r2`` -> ``r2<>r1``. Intros; Red; Intro H0; Rewrite H0 in H; Elim H; Reflexivity. Qed. Lemma Rgt_2_0 : ``0<2``. -Cut ~(O=(2)); [Intro H0; Generalize (lt_INR_0 (2) (neq_O_lt (2) H0)); Unfold INR; Intro H; Assumption | Discriminate]. +Sup0. Qed. Lemma Rgt_3_0 : ``0<3``. -Cut ~(O=(3)); [Intro H0; Generalize (lt_INR_0 (3) (neq_O_lt (3) H0)); Rewrite INR_eq_INR2; Unfold INR2; Intro H; Assumption | Discriminate]. +Sup0. Qed. -(*********************) -(* Lemmes techniques *) -(*********************) - Lemma tech1 : (An:nat->R;N:nat) ((n:nat)``(le n N)``->``0<(An n)``) -> ``0 < (sum_f_R0 An N)``. Intros; Induction N. Simpl; Apply H. @@ -382,6 +378,7 @@ Replace ``k+(1-k)`` with R1; [Assumption | Ring]. Apply Rlt_Rinv; Apply Rgt_2_0. Qed. +Definition SigT := Specif.sigT. (*************************************************) (* Différentes versions du critère de D'Alembert *) |