diff options
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. |