diff options
Diffstat (limited to 'theories/Reals/R_Ifp.v')
| -rw-r--r-- | theories/Reals/R_Ifp.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v index 5365e04000..5f0747d869 100644 --- a/theories/Reals/R_Ifp.v +++ b/theories/Reals/R_Ifp.v @@ -14,7 +14,7 @@ (**********************************************************) Require Import Rbase. -Require Import Omega. +Require Import Lia. Local Open Scope R_scope. (*********************************************************) @@ -60,7 +60,7 @@ Proof. apply lt_IZR in H1. rewrite <- minus_IZR in H2. apply le_IZR in H2. - omega. + lia. Qed. (**********) @@ -230,7 +230,7 @@ Proof. rewrite <- (plus_IZR (Int_part r1 - Int_part r2) 1) in H; generalize (up_tech (r1 - r2) (Int_part r1 - Int_part r2) H0 H); intros; clear H H0; unfold Int_part at 1; - omega. + lia. Qed. (**********) @@ -314,7 +314,7 @@ Proof. in H0; fold (IZR (Int_part r1) - IZR (Int_part r2) - 1) in H0; rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H0; rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H; - auto with zarith real. + auto with real. change (_ + -1) with (IZR (Int_part r1 - Int_part r2) - 1) in H; rewrite (Z_R_minus (Int_part r1 - Int_part r2) 1) in H; rewrite (Z_R_minus (Int_part r1 - Int_part r2) 1) in H0; @@ -323,7 +323,7 @@ Proof. intro; clear H; generalize (up_tech (r1 - r2) (Int_part r1 - Int_part r2 - 1) H1 H0); intros; clear H0 H1; unfold Int_part at 1; - omega. + lia. Qed. (**********) @@ -430,14 +430,14 @@ Proof. clear a b; change 2 with (1 + 1) in H0; rewrite <- (Rplus_assoc (IZR (Int_part r1) + IZR (Int_part r2)) 1 1) in H0; - auto with zarith real. + auto with real. rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H; rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H0; rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H; rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H0; rewrite <- (plus_IZR (Int_part r1 + Int_part r2 + 1) 1) in H0; generalize (up_tech (r1 + r2) (Int_part r1 + Int_part r2 + 1) H H0); - intro; clear H H0; unfold Int_part at 1; omega. + intro; clear H H0; unfold Int_part at 1; lia. Qed. (**********) @@ -499,7 +499,7 @@ Proof. rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H1; generalize (up_tech (r1 + r2) (Int_part r1 + Int_part r2) H0 H1); intro; clear H0 H1; unfold Int_part at 1; - omega. + lia. Qed. (**********) @@ -522,7 +522,7 @@ Proof. rewrite (Rplus_assoc (r1 + r2) (- (IZR (Int_part r1) + IZR (Int_part r2))) (-(1))) ; rewrite <- (Ropp_plus_distr (IZR (Int_part r1) + IZR (Int_part r2)) 1); - trivial with zarith real. + trivial with real. Qed. (**********) |