diff options
| author | Pierre-Marie Pédrot | 2018-09-11 11:46:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-11 11:46:10 +0200 |
| commit | 2f0e274a1436b477e0be0be94a36ee9461a89767 (patch) | |
| tree | 536189bce5ef6f21565fb32534bae11cc37ead2a /theories/Numbers | |
| parent | f3475cd1a68f632b1e6522975354c7dcc1acd6bb (diff) | |
| parent | ddc25ec6150005e949442d422549fbc213d8f4af (diff) | |
Merge PR #8425: Deprecate romega in favor of lia
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Cyclic31.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index ec480bb1eb..4a1f24b95e 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -21,7 +21,7 @@ Require Import Znumtheory. Require Import Zgcd_alt. Require Import Zpow_facts. Require Import CyclicAxioms. -Require Import ROmega. +Require Import Lia. Local Open Scope nat_scope. Local Open Scope int31_scope. @@ -1237,7 +1237,7 @@ Section Int31_Specs. destruct (Z_lt_le_dec (X+Y) wB). contradict H1; auto using Zmod_small with zarith. rewrite <- (Z_mod_plus_full (X+Y) (-1) wB). - rewrite Zmod_small; romega. + rewrite Zmod_small; lia. generalize (Z.compare_eq ((X+Y) mod wB) (X+Y)); intros Heq. destruct Z.compare; intros; @@ -1261,7 +1261,7 @@ Section Int31_Specs. destruct (Z_lt_le_dec (X+Y+1) wB). contradict H1; auto using Zmod_small with zarith. rewrite <- (Z_mod_plus_full (X+Y+1) (-1) wB). - rewrite Zmod_small; romega. + rewrite Zmod_small; lia. generalize (Z.compare_eq ((X+Y+1) mod wB) (X+Y+1)); intros Heq. destruct Z.compare; intros; @@ -1299,8 +1299,8 @@ Section Int31_Specs. unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros. destruct (Z_lt_le_dec (X-Y) 0). rewrite <- (Z_mod_plus_full (X-Y) 1 wB). - rewrite Zmod_small; romega. - contradict H1; apply Zmod_small; romega. + rewrite Zmod_small; lia. + contradict H1; apply Zmod_small; lia. generalize (Z.compare_eq ((X-Y) mod wB) (X-Y)); intros Heq. destruct Z.compare; intros; @@ -1318,8 +1318,8 @@ Section Int31_Specs. unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros. destruct (Z_lt_le_dec (X-Y-1) 0). rewrite <- (Z_mod_plus_full (X-Y-1) 1 wB). - rewrite Zmod_small; romega. - contradict H1; apply Zmod_small; romega. + rewrite Zmod_small; lia. + contradict H1; apply Zmod_small; lia. generalize (Z.compare_eq ((X-Y-1) mod wB) (X-Y-1)); intros Heq. destruct Z.compare; intros; @@ -1356,7 +1356,7 @@ Section Int31_Specs. change [|1|] with 1; change [|0|] with 0. rewrite <- (Z_mod_plus_full (0-[|x|]) 1 wB). rewrite Zminus_mod_idemp_l. - rewrite Zmod_small; generalize (phi_bounded x); romega. + rewrite Zmod_small; generalize (phi_bounded x); lia. Qed. Lemma spec_pred_c : forall x, [-|sub31c x 1|] = [|x|] - 1. |