diff options
Diffstat (limited to 'theories/ZArith/Zlogarithm.v')
| -rw-r--r-- | theories/ZArith/Zlogarithm.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v index ba6d21c4d..30065d705 100644 --- a/theories/ZArith/Zlogarithm.v +++ b/theories/ZArith/Zlogarithm.v @@ -236,7 +236,7 @@ Fixpoint Is_power (p:positive) : Prop := end. Lemma Is_power_correct : - forall p:positive, Is_power p <-> ( exists y : nat | p = shift_nat y 1). + forall p:positive, Is_power p <-> (exists y : nat, p = shift_nat y 1). split; [ elim p; |