Coq Import problems with power

Question

• It seems I can't get the Coq Import system right.
• I found pow_succ_r in Coq.Arith.PeanoNat.
• So I imported it and hoped it is usable

Require Import Coq.Arith.PeanoNat.
Print pow_succ_r.

I get the following error:

pow_succ_r not a defined object.

Answer 1

Notice the line Module Nat near the top of the documentation. It means that the subsequent declarations are inside the Nat module. So, you can access the symbol as Nat.pow_succ_r.

In general, if you are looking for a symbol, use the Locate command:

Locate pow_succ_r.
(*
Constant
  Coq.Arith.PeanoNat.Nat.pow_succ_r
  (shorter name to refer to it in current context is Nat.pow_succ_r)
*)