diff options
| author | Maxime Dénès | 2017-06-14 00:11:00 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-14 00:11:00 +0200 |
| commit | 13d23aafe01f87bdbf2205217b82b7836661c5de (patch) | |
| tree | 873a84dbccc56f5d2f53b3a70161b25b6ac4a676 /theories/Numbers/Cyclic/ZModulo | |
| parent | 25462addaf604ff51e886bbc92937bb272982b04 (diff) | |
| parent | 268ccbb0d3d990e42cef4ae4833e0e7964aea24d (diff) | |
Merge PR#498: Bignums as a separate opam package
Diffstat (limited to 'theories/Numbers/Cyclic/ZModulo')
| -rw-r--r-- | theories/Numbers/Cyclic/ZModulo/ZModulo.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index 04fc5a8dfa..a3d7edbf4b 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -18,7 +18,7 @@ Set Implicit Arguments. Require Import Bool. Require Import ZArith. Require Import Znumtheory. -Require Import BigNumPrelude. +Require Import Zpow_facts. Require Import DoubleType. Require Import CyclicAxioms. @@ -48,13 +48,14 @@ Section ZModulo. Lemma spec_more_than_1_digit: 1 < Zpos digits. Proof. - generalize digits_ne_1; destruct digits; auto. + generalize digits_ne_1; destruct digits; red; auto. destruct 1; auto. Qed. Let digits_gt_1 := spec_more_than_1_digit. Lemma wB_pos : wB > 0. Proof. + apply Z.lt_gt. unfold wB, base; auto with zarith. Qed. Hint Resolve wB_pos. @@ -558,7 +559,7 @@ Section ZModulo. apply Zmod_small. generalize (Z_mod_lt [|w|] (2 ^ [|p|])); intros. split. - destruct H; auto with zarith. + destruct H; auto using Z.lt_gt with zarith. apply Z.le_lt_trans with [|w|]; auto with zarith. apply Zmod_le; auto with zarith. Qed. |