diff options
| -rw-r--r-- | theories/Numbers/NatInt/NZPow.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v index 01a15686e0..3b2a496229 100644 --- a/theories/Numbers/NatInt/NZPow.v +++ b/theories/Numbers/NatInt/NZPow.v @@ -238,7 +238,7 @@ Qed. Lemma pow_le_mono : forall a b c d, 0<a<=c -> b<=d -> a^b <= c^d. Proof. - intros. transitivity (a^d). + intros a b c d ? ?. transitivity (a^d). - apply pow_le_mono_r; intuition order. - apply pow_le_mono_l; intuition order. Qed. |