Insert a structure of uniform space

[drouhling]

This is meant to replace #119.

Some lemmas can be generalised (from pseudometric to uniform) as in #119 but this should be in another PR.

[CohenCyril]

That's great!!

• @drouhling can you add a CHANGELOG_UNRELEASED.md entry?
• @pi8027 can you verify the new hierarchy?

[pi8027]

@CohenCyril @drouhling Done, but I didn't check the implementation by myself yet. There are 5 missing joins:

Fail check_join CompletePseudoMetric.type GRing.Lmodule.type CompleteNormedModule.type.
Fail check_join CompletePseudoMetric.type GRing.Zmodule.type CompleteNormedModule.type.
Fail check_join CompletePseudoMetric.type NormedModule.type CompleteNormedModule.type.
Fail check_join CompletePseudoMetric.type Num.NormedZmodule.type CompleteNormedModule.type.
Fail check_join CompletePseudoMetric.type PseudoMetricNormedZmodule.type CompleteNormedModule.type.

[drouhling]

* @drouhling can you add a `CHANGELOG_UNRELEASED.md` entry?

Done.

Fail check_join CompletePseudoMetric.type GRing.Lmodule.type CompleteNormedModule.type.
Fail check_join CompletePseudoMetric.type GRing.Zmodule.type CompleteNormedModule.type.
Fail check_join CompletePseudoMetric.type NormedModule.type CompleteNormedModule.type.
Fail check_join CompletePseudoMetric.type Num.NormedZmodule.type CompleteNormedModule.type.
Fail check_join CompletePseudoMetric.type PseudoMetricNormedZmodule.type CompleteNormedModule.type.

I added the missing joins.

[drouhling]

In addition to the asked modifications, I updated the misc/uniform_bigO.v file.

[pi8027]

Now the new hierarchy is correct. :)