Splitting normedmodtype.v

[mkerjean]

Normedmodtype.v is a long file, and this triggers several issues, alike the one descripe in Issue#1167 advocating the spit of topology.v.

• Compilation takes a long time, when trying to add a lemma.
• The file mixes several new structures and adding an intermediate structure as in PR#1300 is complicated, maybe unecessary so.

As far as I can see, I see five parts in this file, not well ordered:

• PseudoMetricNormedZmodules depending on numDomains
• PseudoMetricNormedZmod depending on numFieldType
• NormedModules depending on numDomains
• NormModules depending on numFieldTypes
• Theorems about realFied, in the last sections.

In particular, some lemmas about PseudoMetricNormedZmod depending on numFieldType (as add_continuous) are proved quite late, after the introduction of NormedModules. I am not sure yet normedmodtype.v can be separated in 5 files, happy to discuss a better way to split it.