diff options
| author | Frédéric Besson <frederic.besson@inria.fr> | 2020-01-20 22:04:18 (GMT) |
|---|---|---|
| committer | Frédéric Besson <frederic.besson@inria.fr> | 2020-01-20 22:29:17 (GMT) |
| commit | 10fe534afc1b0441dbe4ac8c35840283f1136b41 (patch) | |
| tree | 9ddc149e06e707e2faa4b71ff491b7a8d6761d5b /test-suite | |
| parent | ab266eee94d82a3f957c1a85c77a23c18e75991f (diff) | |
| download | coq-10fe534afc1b0441dbe4ac8c35840283f1136b41.zip coq-10fe534afc1b0441dbe4ac8c35840283f1136b41.tar.gz coq-10fe534afc1b0441dbe4ac8c35840283f1136b41.tar.bz2 | |
[zify] quick fix of #11191refs/pull/11430/head
Z.pow_pos is defined in the separate ZifyPow.v
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/micromega/bug_11191.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/micromega/bug_11191.v b/test-suite/micromega/bug_11191.v new file mode 100644 index 0000000..e1581cb --- /dev/null +++ b/test-suite/micromega/bug_11191.v @@ -0,0 +1,11 @@ +Require Import ZArith Lia. + +Goal forall p, (0 < Z.pos (p ^ 2))%Z. + intros. + lia. +Qed. + +Goal forall p n, (0 < Z.pos (p ^ n))%Z. + intros. + lia. +Qed. |