I'm trying to understand the scoping of Coq. I'd need Nat2Z.inj_pow in a proof of mine, and https://coq.inria.fr/library/Coq.ZArith.Znat.html tells that such a module has such a lemma.

So, I've done

```
Require Import BinNums.
Require Import Coq.ZArith.BinInt.
Require Import Coq.ZArith.Znat.
```

For some reason, Coq doesn't find the lemma (or anything else) in Nat2Z, but does in a few other submodules there. `Search "inj_pow".`

shows these lemmas named inj_pow:

```
Pos2Z.inj_pow: ∀ p q : positive, Z.pos (p ^ q) = (Z.pos p ^ Z.pos q)%Z
N2Z.inj_pow: ∀ n m : N, Z.of_N (BinNat.N.pow n m) = (Z.of_N n ^ Z.of_N m)%Z
Zabs2N.inj_pow: ∀ n m : Z, (0 <= m)%Z → Z.abs_N (n ^ m) = BinNat.N.pow (Z.abs_N n) (Z.abs_N m)
Z2N.inj_pow: ∀ n m : Z, (0 <= n)%Z → (0 <= m)%Z → Z.to_N (n ^ m) = BinNat.N.pow (Z.to_N n) (Z.to_N m)
Z2Pos.inj_pow: ∀ x y : Z, (0 < x)%Z → (0 < y)%Z → Z.to_pos (x ^ y) = (Z.to_pos x ^ Z.to_pos y)%positive
```

What am I missing?

It seems your link is about Coq 8.14, which has more `inj_pow`

lemmas in that specific file than (say) Coq 8.13 (on which I can reproduce your symptoms).

indeed, comparing https://coq.github.io/doc/v8.13/stdlib/Coq.ZArith.Znat.html vs https://coq.github.io/doc/v8.14/stdlib/Coq.ZArith.Znat.html seems to agree; the change seems to have happened as part of the `lia`

improvements in https://github.com/coq/coq/pull/14037.

Ah, that makes sense. Thank you :)

Sami Liedes has marked this topic as resolved.

Last updated: Jun 24 2024 at 12:02 UTC