diff options
| author | Pierre Letouzey | 2017-03-22 11:24:27 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2017-06-13 10:30:29 +0200 |
| commit | 295107103aaa86db8a31abb0e410123212648d45 (patch) | |
| tree | 15928f2d0e3752e70938401555faddb48661f34d /theories/Numbers/Cyclic/ZModulo | |
| parent | 423d3202fa0f244db36a0b1b45edfa61829201e6 (diff) | |
BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)
See now https://github.com/coq/bignums
Int31 is still in the stdlib.
Some proofs there has be adapted to avoid the need for BigNumPrelude.
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. |