I usually import QArith.
If I write
Search "max" "id".
Then I can see something like this:
Pos.max_id: forall n : positive, Pos.max n n = n
N.max_id: forall n : N, N.max n n = n
Nat.max_id: forall n : nat, Nat.max n n = n
Z.max_id: forall n : Z, Z.max n n = n
If I write
Search "Pos" "max".
Then nothing appears.
How can I search another (included?) library (or module) 's lemma?