How to avoid necessity to put module prefix

Before now I was editing IndProp.v file from Software foundations. But as soon as I put the code into a separate file I found that eqb_neq command requires a module prefix to work: Nat.eqb_neq.

Here is the code:

Set Warnings "-notation-overridden,-parsing".
Require Import List.
Import ListNotations.
Require Import PeanoNat.
Local Open Scope nat_scope.

Inductive nostutter {X:Type} : list X -> Prop :=
| ns_nil : nostutter []
| ns_one : forall (x : X), nostutter [x]
| ns_cons: forall (x : X) (h : X) (t : list X), nostutter (h::t) -> x <> h -> nostutter (x::h::t).

Example test_nostutter_1: nostutter [3;1;4;1;5;6].
Proof.
  repeat constructor; apply Nat.eqb_neq; auto.
Qed.

Is it possible to tell coq that I am always using Nat module here and get rid of Nat prefix? Like in C++ you can write using namespace std; and there will be no need to explicitly specify the namespace before every object from it.

Solution

You can use Import Nat. to do that. But this can harm readability sometimes. Some modules are designed to be used with their prefixes, e.g. stdlib's Vector.