test-suite/micromega/bug_12184.v


1
2
3
4
5
6
7
8

Require Import Lia.
Require Import ZArith.

Goal forall p : positive, (0 < Z.pos (2^p)%positive)%Z.
Proof.
  intros p.
  lia.
Qed.