diff options
Diffstat (limited to 'theories/Reals/Machin.v')
| -rw-r--r-- | theories/Reals/Machin.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Reals/Machin.v b/theories/Reals/Machin.v index 08bc38a085..d5a39f527f 100644 --- a/theories/Reals/Machin.v +++ b/theories/Reals/Machin.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Omega. +Require Import Lia. Require Import Lra. Require Import Rbase. Require Import Rtrigo1. @@ -163,8 +163,8 @@ assert (cv : Un_cv PI_2_3_7_tg 0). rewrite <- (Rmult_0_r 2), <- Ropp_mult_distr_r_reverse. rewrite <- Rmult_plus_distr_l, Rabs_mult, (Rabs_pos_eq 2);[|lra]. rewrite Rmult_assoc; apply Rmult_lt_compat_l;[lra | ]. - apply (Pn1 n); omega. - apply (Pn2 n); omega. + apply (Pn1 n); lia. + apply (Pn2 n); lia. rewrite Machin_2_3_7. rewrite !atan_eq_ps_atan; try (split; lra). unfold ps_atan; destruct (in_int (/3)); destruct (in_int (/7)); |