The command Import is not sufficient. Indeed, if one wants to use twice
the same module, it is necessary to rename the different objects it can
contains to have distinct copies of them.
To do this, you can use the command Use (see the index of commands for
its complete syntax and the definition of renaming). The different
possibilities of renaming, and a careful choice of names allow you to
transform easily the names declared in the module you want to use.
When you use a module, you sometimes know that you are not extending the
theory. For instance, if you prove that a structure satisfies all the group
axioms, you can load the group module to use all the theorems about groups and
you are not extending the theory. The -n option of the Use command
checks that it is the case and an error will result if you extend the theory.
Important note: there is an important difference between Use and Import other than the possibility of renaming with Use. When you apply
a renaming to a module foo this renaming does not apply to the module
imported by foo (with Import) but it applies to the module used
by foo (with Use). This allows you to import modules like natural
numbers when developing other theories with a default behaviour which is not
to rename objects from the natural numbers theory when your module is used.
You can override this default behaviour (see the index of commands), but it is
very seldom useful.