WIP: Sketch some theory about euclidean spaces

Formalize Eucl.Spaces using `R∞`
This way, we have the following benefits:
* All vectors of euclidean spaces use the same operations and live in
the same type. They are inter-compatible.
* We don't have to deal with the difficult induction schemes of
`Vector.t` or have to prove preservation of length for list operations.
* We also get a canonical (with respect to this library) instance of the
`ℝ^ℕ` topology.

Further stuff:
* Prove continuity of `Rinfty_add`, `Rinfty_scale`, `Rn_projection`,
`Rinfty_scalarproduct`.
* Linear subspaces have to be nonempty, thus include zero.
* Some proofs. Including: a linear combination stays inside the
subspace its vectors come from. A linear combination can be reduced to a
list without repetitions of vectors. The unit vectors are linearly
independent.

_CoqProject

@@ -9,6 +9,7 @@ theories/Topology/Connectedness.v
 theories/Topology/Continuity.v
 theories/Topology/ContinuousFactorization.v
 theories/Topology/CountabilityAxioms.v
+theories/Topology/EuclideanSpaces.v
 theories/Topology/FilterLimits.v
 theories/Topology/FiltersAndNets.v
 theories/Topology/Homeomorphisms.v