diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-15 15:35:04 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-15 15:35:04 +0000 |
| commit | fea0a3265a7191a7e8c13028e7edd9bf29ba4d25 (patch) | |
| tree | f0993cfb172fd6e3cd280fcebf61ac0d6dc3e71b /theories/Reals/Exp_prop.v | |
| parent | d72eb6e333f710bb8f4ea0061e8399aafba19fe0 (diff) | |
Nouvelle interprétation des nombres réels
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3499 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Exp_prop.v')
| -rw-r--r-- | theories/Reals/Exp_prop.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index ae6433466..3c2b16f10 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -381,6 +381,7 @@ Repeat Rewrite <- Rmult_assoc. Rewrite <- Rinv_r_sym. Rewrite Rmult_1l. Replace ``(INR N)*(INR N)`` with (Rsqr (INR N)); [Idtac | Reflexivity]. +Rewrite Rmult_assoc. Rewrite Rmult_sym. Replace ``4`` with (Rsqr ``2``); [Idtac | SqRing]. Rewrite <- Rsqr_times. @@ -576,8 +577,9 @@ Apply RmaxLess1. Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. DiscrR. Apply Rle_sym1. -Unfold Rdiv; Repeat Apply Rmult_le_pos. +Unfold Rdiv; Apply Rmult_le_pos. Left; Sup0. +Apply Rmult_le_pos. Apply pow_le. Apply Rle_trans with R1. Left; Apply Rlt_R0_R1. |