Add homeomorphism example - see #25.

Only since v8.13 is it possible to use `apply` on multiple hypotheses
simultaneously.

The functions `curry` and `uncurry` only exist since Coq v8.13 and were
earlier called `prod_uncurry` and `prod_curry`. But the latter got
deprecated. To ensure compatibility with Coq v8.12 (and simplifying the
code a little when using `f1` but complicating the def. of `f1`) the
definition of `f1` is changed a little.

This theorem is only available in Coq v8.13 and later. To stay
compatible with Coq v8.12, this theorem has to be avoided.

Author: stop-cran

_CoqProject

@@ -36,6 +36,7 @@ theories/Topology/TopologicalSpaces.v
 theories/Topology/UniformTopology.v
 theories/Topology/UrysohnsLemma.v
 theories/Topology/WeakTopology.v
+theories/Topology/Examples/S1.v
 theories/ZornsLemma/Cardinals.v
 theories/ZornsLemma/Classical_Wf.v
 theories/ZornsLemma/CountableTypes.v