diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-06 16:57:31 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-06 16:57:31 +0000 |
| commit | c80fbaac51c390d11e75763cd67b999eb8a671ff (patch) | |
| tree | 9982f2d6e601d1fe4f75e7bee7b9347d524da0a2 /theories/Reals/Rfunctions.v | |
| parent | 46f35c939cb0a17b68a0aef8119c73a6c1144a4d (diff) | |
Renoncement à rationaliser les Hints "real" vis à vis de Rle/Rge et Rlt/Rgt :
- si on met Rle_ge et Rge_le tous les deux en Resolve (et de même
pour Rlt_gt et Rgt_lt) alors on introduit un cycle,
- si on en met un des deux en Immediate, alors on perd la symétrie car si
un développement n'a un lemme en hints que pour Rge (resp Rle),
alors il ne sera pas utilisable si on met Rge_le (resp Rle_ge) en Immediate
(et c'est ce qui arrive notamment dans HighSchoolGeometry).
L'idéal serait d'introduire une notion de raisonnement modulo équivalence
dans auto afin que chaque lemme sur Rle (resp Rge) soit systématiquement
applicable aussi face à Rge (resp Rle) sans redondances et sans
cycle. Ainsi Rle_ge and co n'auraient pas un statut de hints mais plutôt un
statut de conversions implicites entre notions synonymes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10762 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rfunctions.v')
| -rw-r--r-- | theories/Reals/Rfunctions.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index db2a0390f..da28184f2 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -349,7 +349,7 @@ Proof. rewrite Rabs_Rinv; auto. rewrite <- Rinv_pow; auto. rewrite RPow_abs; auto. - rewrite H'0; rewrite Rabs_right; auto with real. + rewrite H'0; rewrite Rabs_right; auto with real rorders. apply Rlt_pow; auto with arith. rewrite Rabs_Rinv; auto. apply Rmult_lt_reg_l with (r := Rabs r). |