Requires should always be at the top of a file, Imports can be inside
of submodules.

It is strange that a Require in a submodule is allowed and then triggers
an error when using the whole module. This may be a Coq bug.