diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-07-06 13:48:40 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-07-06 13:48:40 -0400 |
| commit | cc920cf2a3aa859a93e8e990a19a960f78cd3b1b (patch) | |
| tree | ed93d93f82578239ef2e0a6843e52e1d6968a5ef /src/BaseSystem.v | |
| parent | 260b20cab885deae59a305492567dc0f0d88b3a8 (diff) | |
| parent | 0cea3e2f80408a25954f820faebf5cd79d2e13ae (diff) | |
Merged changes, including new ZUtil conventions.
Diffstat (limited to 'src/BaseSystem.v')
| -rw-r--r-- | src/BaseSystem.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/BaseSystem.v b/src/BaseSystem.v index a37932de0..0ad6c0a03 100644 --- a/src/BaseSystem.v +++ b/src/BaseSystem.v @@ -120,7 +120,7 @@ Section PolynomialBaseCoefs. rewrite in_map_iff in *. destruct H; destruct H. subst. - apply pos_pow_nat_pos. + apply Z.pos_pow_nat_pos. Qed. Lemma poly_base_defn : forall i, (i < length poly_base)%nat -> @@ -145,7 +145,6 @@ Section PolynomialBaseCoefs. with (Z.pos b1); auto. rewrite Z_div_mult_full; auto. apply Z.pow_nonzero; intuition. - pose proof (Zgt_pos_0 b1); omega. Qed. Lemma poly_base_good: |