Coq is using a module system similar to OCaml. In OCaml, we can apply a function like Module_A.Module_B.Func and use Module_A.Module_B. to find the path to Func.
However, I cannot do similar things in Coq. For instance, if I just run Print Coq.Arith.Minus.minus_n_O. Coq reports Coq.Arith.Minus.minus_n_O is not a defined object.
I must first load the library and then can print the object. In the following case, it is successful.
From Coq Require Export Arith.Minus.
Print Coq.Arith.Minus.minus_n_O.
Is there a way to run Print Coq.Arith.Minus.minus_n_O without loading the library just as applying a function in OCaml?
In Coq there is a distinction between requiring and importing a module. Require is the keyword that lets you load the library while Import lets you drop the prefix. Export M does Import M but also says that when the current module is itself imported, then M will be imported too.
I would say what you want is
From Coq Require Arith.Minus.
Print Coq.Arith.Minus.minus_n_O.
without the Export.
To compare with ocaml, Import is like open and Require is just implicit in ocaml: a module is imported when it is used basically.
You can find more in the documentation of Import, Export and Require. Also in general to find more about commands, just look up the command index.