diff --git a/.travis.yml b/.travis.yml
new file mode 100644
index 000000000..6df16b626
--- /dev/null
+++ b/.travis.yml
@@ -0,0 +1,31 @@
+language: generic
+os: linux
+
+branches:
+  only:
+  - master
+
+services:
+- docker
+
+env:
+  global:
+  - NJOBS="2"
+  - CONTRIB="analysis"
+  - OPAMYES=yes
+  jobs:
+  - DOCKERIMAGE="mathcomp/mathcomp:1.11.0-coq-8.10"
+  - DOCKERIMAGE="mathcomp/mathcomp:1.11.0-coq-8.11"
+  - DOCKERIMAGE="mathcomp/mathcomp:1.11.0-coq-8.12"
+
+install:
+- docker pull ${DOCKERIMAGE}
+- docker tag  ${DOCKERIMAGE} ci:current
+- docker run  --env=OPAMYES --init -id --name=CI -v ${TRAVIS_BUILD_DIR}:/home/coq/${CONTRIB} -w /home/coq/${CONTRIB} ci:current
+- docker exec CI /bin/bash --login -c "opam repo add coq-released https://coq.inria.fr/opam/released"
+- docker exec CI /bin/bash --login -c "opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev"
+# - docker exec CI /bin/bash --login -c "opam pin add -y -n coq-mathcomp-${CONTRIB} ."
+- docker exec CI /bin/bash --login -c "opam install --deps-only ."
+
+script:
+- docker exec CI /bin/bash --login -c "opam install -vvv ."
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 699bb8945..d709d8ed0 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -52,6 +52,51 @@
 - in `lebesgue_integral_differentiation.v`:
   + lemma `nicely_shrinking_fin_num`
 
+- in `unstable.v`
+  + lemmas `scalecE`, `normcr`, `Im_mul`, `mulrnc`, `complexA`, `normc_natmul`,
+    `nomrc_mulrn`, `gt0_normc`, `gt0_realC`, `ltc0E`, `ltc0P`, `ltcP`, `lecP`,
+    `realC_gt0`, `Creal_gtE`, `realC_norm`, `eqCr`, `eqCI`, `neqCr0`,
+    `real_normc_ler`, `im_normc_ler`
+  + notations `f %:Rfun`, `v %:Rc`
+  + lemmas `realCZ`, `realC_alg`, `scalecr`, `scalecV`
+
+- in `function_spaces.v`
+  + lemmas `cvg_big`, `continuous_big`
+
+- file `holomorphy.v`
+  + instance of `normedModType` on `complex`
+  + definition `ball_Rcomplex`
+  + lemmas `entourage_RcomplexE`, `normcZ`, `Rcomplex_findim`
+  + instance of `normedVectType` on `complex`
+  + definitions `holomorphic`, `Rdifferentiable`, `realC`, `CauchyRiemannEq`
+  + lemmas `holomorphicP`, `continuous_realC`, `Rdiff1`, `Rdiffi`, `littleoCo`,
+    `holo_differentiable`, `holo_CauchyRiemann`, `Diff_CR_holo`,
+    `holomorphic_Rdiff`
+
+- in `landau.v`
+  + lemma `littleoE0`
+
+- in `normed_module.v`
+  + structure `normedVectType`
+  + lemmas `dnbhs0_le`, `nbhs0_le`, `dnbrg0_lt`, `nbhs0_lt`
+  + definition `pseudometric`
+  + instance of `normedZmodType`, `pointedType` and `pseudoMetricType`
+    on `pseudometric`
+  + definitions `oo_norm`, `oo_space`,
+  + instance of `normedModType` on `oo_space`
+  + lemmas `oo_closed_ball_compact`, `equivalence_norms`,
+    `linear_findim_continuous`
+
+- in `num_topology.v`
+  + instance of `pseudoMetricType` on `GRing.regular`
+
+- in `uniform_structure`
+  + lemma `within_continuous_withinNx`
+
+- in `tvs.v`
+  + lemmas `cvg_sum`, `sum_continuous`, `entourage_nbhsE`
+  + instance of `UniformZmodule.type` on `GRing.regular`
+
 ### Changed
 
 - in `convex.v`:
diff --git a/_CoqProject b/_CoqProject
index 4bd2a3f29..9bd30d25b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -97,6 +97,7 @@ theories/forms.v
 theories/derive.v
 theories/measure.v
 theories/numfun.v
+theories/holomorphy.v
 
 theories/lebesgue_integral_theory/simple_functions.v
 theories/lebesgue_integral_theory/lebesgue_integral_definition.v
diff --git a/classical/unstable.v b/classical/unstable.v
index 563dcb989..780bad49b 100644
--- a/classical/unstable.v
+++ b/classical/unstable.v
@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
-From mathcomp Require Import archimedean finset interval mathcomp_extra.
+From mathcomp Require Import archimedean finset interval complex mathcomp_extra.
 
 (**md**************************************************************************)
 (* # MathComp extra                                                           *)
@@ -33,6 +33,7 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Import Order.TTheory GRing.Theory Num.Theory.
+Local Open Scope complex_scope.
 Local Open Scope ring_scope.
 
 Section ssralg.
@@ -483,3 +484,131 @@ Notation " R ~~> R' " := (@respectful _ _ (Program.Basics.flip (R%signature)) (R
 
 Export -(notations) Morphisms.
 End ProperNotations.
+
+(* TODO: backport to real-closed *)
+Section complex_extras.
+Variable R : rcfType.
+Local Notation sqrtr := Num.sqrt.
+Local Notation C := R[i].
+
+Import Normc.
+Import Num.Def.
+Import complex.
+
+Lemma scalecE (w  v : C) : v *: w = v * w.
+Proof. by []. Qed.
+
+(* FIXME: unused *)
+Lemma normcr (x : R) : normc (x%:C) = normr x.
+Proof. by rewrite /normc/= expr0n //= addr0 sqrtr_sqr. Qed.
+
+Lemma Im_mul (x : R) : x *i = x%:C * 'i%C.
+Proof. by simpc. Qed.
+
+Lemma mulrnc (a b : R) k : a +i* b *+ k = (a *+ k) +i* (b *+ k).
+Proof.
+by elim: k => // k ih; apply/eqP; rewrite !mulrS eq_complex !ih !eqxx.
+Qed.
+
+Lemma complexA (h : C) : h%:A = h.
+Proof. by rewrite scalecE mulr1. Qed.
+
+Lemma normc_natmul (k : nat) : normc k%:R = k%:R :> R.
+Proof. by rewrite mulrnc /= mul0rn expr0n addr0 sqrtr_sqr normr_nat. Qed.
+
+Lemma normc_mulrn (x : C) k : normc (x *+ k) = (normc x) *+ k.
+Proof.
+by rewrite -mulr_natr normcM -[in RHS]mulr_natr normc_natmul.
+Qed.
+
+Lemma gt0_normc (r : C) : 0 < r -> r = (normc r)%:C.
+Proof.
+case: r => x y /= /andP[] /eqP -> x0.
+by rewrite expr0n addr0 sqrtr_sqr gtr0_norm.
+Qed.
+
+Lemma gt0_realC (r : C) : 0 < r -> r = (Re r)%:C.
+Proof. by case: r => x y /andP[] /eqP -> _. Qed.
+
+Lemma ltc0E  (k : R): (0 < k%:C) = (0 < k).
+Proof. by simpc. Qed.
+
+Lemma ltc0P  (k : R): (0 < k%:C) <-> (0 < k).
+Proof. by simpc. Qed.
+
+Lemma ltcP  (k t: R): (t%:C < k%:C) <-> (t < k).
+Proof. by simpc. Qed.
+
+Lemma lecP  (k t: R): (t%:C <= k%:C) <-> (t <= k).
+Proof. by simpc. Qed.
+
+(* (*TBA algC *) *)
+Lemma realC_gt0 (d : C) : 0 < d -> (0 < Re d :> R).
+Proof. by rewrite ltcE => /andP [] //. Qed.
+
+Lemma Creal_gtE (c d : C) : c < d -> (complex.Re c < complex.Re d).
+Proof. by rewrite ltcE => /andP [] //. Qed.
+
+Lemma realC_norm (b : R) : `|b%:C| = `|b|%:C.
+Proof. by rewrite normc_def /= expr0n addr0 sqrtr_sqr. Qed.
+
+Lemma eqCr (r s : R) : (r%:C == s%:C) = (r == s).
+Proof. exact: (inj_eq (@complexI _)). Qed.
+
+Lemma eqCI (r s : R) : (r *i == s *i) = (r == s).
+Proof. by apply/idP/idP => [/eqP[] ->//|/eqP ->]. Qed.
+
+Lemma neqCr0 (r : R) : (r%:C != 0) = (r != 0).
+Proof. by apply/negP/negP; rewrite ?eqCr. Qed.
+
+Lemma real_normc_ler (x : C) :
+  `|Re x| <= normc x.
+Proof.
+case: x => x y /=.
+rewrite -ler_sqr ?nnegrE ?normr_ge0 ?sqrtr_ge0 //.
+rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=.
+by rewrite lerDl ?sqr_ge0.
+Qed.
+
+Lemma im_normc_ler (x : C) :
+  `|Im x| <= normc x.
+Proof.
+case: x => x y /=.
+rewrite -ler_sqr ?nnegrE ?normr_ge0 ?sqrtr_ge0 //.
+rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=.
+by rewrite lerDr ?sqr_ge0.
+Qed.
+
+End complex_extras.
+
+Notation  "f %:Rfun" :=
+  (f : (Rcomplex _) -> (Rcomplex _))
+  (at level 5,  format "f %:Rfun")  : complex_scope.
+
+Notation  "v %:Rc" :=   (v : (Rcomplex _))
+                          (at level 5, format "v %:Rc")  : complex_scope.
+
+Section algebraic_lemmas.
+Variable (R: rcfType).
+Notation C := R[i].
+Notation Rcomplex := (Rcomplex R).
+
+Import Normc.
+
+Lemma realCZ (a : R) (b : Rcomplex) : a%:C * b = a *: b.
+Proof. by case: b => x y; simpc. Qed.
+
+Lemma realC_alg (a : R) : a *: (1%:Rc) = a%:C.
+Proof. by rewrite /GRing.scale/= mulr1 mulr0. Qed.
+
+Lemma scalecr (w: C) (r : R) : r *: (w: Rcomplex) = r%:C *: w .
+Proof. by case w => a b; simpc. Qed.
+
+Lemma scalecV (h: R) (v: Rcomplex):
+  h != 0 -> v != 0 -> (h *: v)^-1 = h^-1 *: v^-1. (* scaleCV *)
+Proof.
+by move=> h0 v0; rewrite scalecr invrM // ?unitfE ?eqCr // mulrC scalecr fmorphV.
+Qed.
+
+End algebraic_lemmas.
+
diff --git a/config.nix b/config.nix
new file mode 100644
index 000000000..87c4d6070
--- /dev/null
+++ b/config.nix
@@ -0,0 +1,6 @@
+{
+  coq = "8.11";
+  mathcomp = "mathcomp-1.12.0";
+  mathcomp-real-closed = "mkerjean/master";
+  mathcomp-finmap = "1.5.1";
+}
diff --git a/opam b/opam
new file mode 100644
index 000000000..e9bd5838b
--- /dev/null
+++ b/opam
@@ -0,0 +1,41 @@
+opam-version: "2.0"
+maintainer: "reynald.affeldt@aist.go.jp"
+homepage: "https://github.com/math-comp/analysis"
+bug-reports: "https://github.com/math-comp/analysis/issues"
+dev-repo: "git+https://github.com/math-comp/analysis.git"
+license: "CECILL-C"
+authors: [
+  "Reynald Affeldt"
+  "Cyril Cohen"
+  "Assia Mahboubi"
+  "Damien Rouhling"
+  "Pierre-Yves Strub"
+]
+build: [
+  [make "INSTMODE=global" "config"]
+  [make "-j%{jobs}%"]
+]
+install: [
+  [make "install"]
+]
+depends: [
+  "coq" { ((>= "8.10" & < "8.13~") | = "dev") }
+  "coq-mathcomp-field"       {(>= "1.11.0" & < "1.12~")}
+  "coq-mathcomp-finmap"      {(>= "1.5.0" & < "1.6~")}
+  "coq-mathcomp-real-closed"          {(>= "1.0.5" & < "1.1~")}
+]
+synopsis: "An analysis library for mathematical components"
+description: """
+This repository contains an experimental library for real analysis for
+the Coq proof-assistant and using the Mathematical Components library.
+
+It is inspired by the Coquelicot library.
+"""
+tags: [
+  "category:Mathematics/Real Calculus and Topology"
+  "keyword: analysis"
+  "keyword: topology"
+  "keyword: real numbers"
+  "logpath: mathcomp.analysis"
+  "date:2020-08-11"
+]
diff --git a/theories/function_spaces.v b/theories/function_spaces.v
index a920e9e63..8451cadee 100644
--- a/theories/function_spaces.v
+++ b/theories/function_spaces.v
@@ -1557,6 +1557,40 @@ End cartesian_closed.
 
 End currying.
 
+Section big_continuous.
+
+Lemma cvg_big (T : Type) (U : topologicalType) [F : set_system T] [I : Type]
+    (r : seq I) (P : pred I) (Ff : I -> T -> U) (Fa : I -> U)
+    (op : U -> U -> U) (x0 : U):
+  Filter F ->
+  continuous (fun x : U * U => op x.1 x.2) ->
+  (forall i, P i -> Ff i x @[x --> F] --> Fa i) ->
+  \big[op/x0]_(i <- r | P i) (Ff i x) @[x --> F] -->
+    \big[op/x0]_(i <- r | P i) Fa i.
+Proof.
+move=> FF opC0 cvg_f.
+elim: r => [|x r IHr].
+  rewrite big_nil.
+  under eq_cvg do rewrite big_nil.
+  exact: cvg_cst.
+rewrite big_cons (eq_cvg _ _ (fun x => big_cons _ _ _ _ _ _)).
+case/boolP: (P x) => // Px.
+apply: (@cvg_comp _ _ _ (fun x1 => (Ff x x1, \big[op/x0]_(j <- r | P j) Ff j x1)) _ _ (nbhs (Fa x, \big[op/x0]_(j <- r | P j) Fa j)) _ _ (continuous_curry_cvg opC0)).
+by apply: cvg_pair => //; apply: cvg_f.
+Qed.
+
+Lemma continuous_big [K T : topologicalType] [I : Type] (r : seq I)
+    (P : pred I) (F : I -> T -> K) (op : K -> K -> K) (x0 : K) :
+  continuous (fun x : K * K => op x.1 x.2) ->
+  (forall i, P i -> continuous (F i)) ->
+  continuous (fun x => \big[op/x0]_(i <- r | P i) F i x).
+Proof.
+move=> op_cont f_cont x.
+by apply: cvg_big => // i /f_cont; apply.
+Qed.
+
+End big_continuous.
+
 Definition eval {X Y : topologicalType} : continuousType X Y * X -> Y :=
   uncurry (id : continuousType X Y -> (X -> Y)).
 
diff --git a/theories/holomorphy.v b/theories/holomorphy.v
new file mode 100644
index 000000000..e9263dd25
--- /dev/null
+++ b/theories/holomorphy.v
@@ -0,0 +1,272 @@
+
+(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(*Require Import ssrsearch.*)
+From HB Require Import structures.
+From mathcomp Require Import ssreflect ssrfun ssrbool fieldext falgebra vector.
+From mathcomp Require Import ssrnat eqtype seq choice fintype bigop order.
+From mathcomp Require Import ssralg ssrnum ssrfun matrix complex.
+From mathcomp Require Import unstable boolp reals ereal derive.
+From mathcomp Require Import classical_sets functions interval_inference.
+From mathcomp Require Import topology normedtype landau.
+
+(**md**************************************************************************)
+(* # Holomorphic functions                                                    *)
+(*                                                                            *)
+(* This file develops the theory of holomorphic functions. We endow complex   *)
+(* (denoted C below) and Rcomplex with structures of normedModType. We prove  *)
+(* that the holomorphic functions are the R-differentiable functions from C   *)
+(* to C satisfying the Cauchy-Riemann equation.                               *)
+(*                                                                            *)
+(*          holomorphic f == f is holomorphic, i.e. C-derivable               *)
+(*      Rdifferentiable f == f is differentiable on Rcomplex                  *)
+(*    CauchyRiemannEq f c == The Cauchy-Riemman equation for f at point c     *)
+(*                                                                            *)
+(******************************************************************************)
+
+Import Order.TTheory GRing.Theory Num.Theory ComplexField Num.Def complex.
+Local Open Scope ring_scope.
+Local Open Scope classical_set_scope.
+Local Open Scope complex_scope.
+Import numFieldNormedType.Exports.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+HB.instance Definition _ (R : rcfType) := NormedModule.copy R[i] R[i]^o.
+HB.instance Definition _ (R : rcfType) := UniformZmodule.copy R[i] R[i]^o.
+
+HB.instance Definition _ (R : rcfType) := UniformZmodule.copy (Rcomplex R) R[i].
+HB.instance Definition _ (R : rcfType) := Pointed.copy (Rcomplex R) R[i].
+
+Module Rcomplex_NormedModType.
+Section Rcomplex_NormedModType.
+Variable (R : rcfType).
+
+Definition ball_Rcomplex : Rcomplex R -> R -> Rcomplex R -> Prop :=
+  ball_ Num.norm.
+
+Lemma entourage_RcomplexE : entourage = entourage_ ball_Rcomplex.
+Proof.
+rewrite entourage_nbhsE/= eqEsubset.
+split; apply/subsetP => U; rewrite inE => -[].
+  move=> V []/= e; rewrite ltcE => /andP[]/eqP/= ei0 e0.
+  have ->: e = (Re e)%:C by case: e ei0 {e0} => r i/= ->.
+  move=> /subsetP eV /subsetP VU.
+  rewrite inE; exists (Re e) => //.
+  apply/subsetP => -[] a b; rewrite inE/= /ball/= => abe.
+  by apply: VU; rewrite inE/=; apply: eV; rewrite inE/= add0r opprB ltcR.
+move=> e/= e0 /subsetP eU.
+rewrite inE; exists (ball_Rcomplex 0 e).
+  exists e%:C; first by rewrite /= ltcR.
+  by apply/subsetP => x; rewrite !inE/= ltcR.
+apply/subsetP => x; rewrite inE/= inE /ball_Rcomplex/= add0r opprB => xe.
+by apply: eU; rewrite inE.
+Qed.
+
+HB.instance Definition _ := Uniform_isPseudoMetric.Build R (Rcomplex R)
+  ball_norm_center ball_norm_symmetric ball_norm_triangle entourage_RcomplexE.
+HB.instance Definition _ :=
+  NormedZmod_PseudoMetric_eq.Build R (Rcomplex R) erefl.
+
+Lemma normcZ (l : R) (x : Rcomplex R) : `|l *: x| = `|l| * `|x|.
+Proof.
+by case: x => ??; rewrite /normr/= !exprMn -mulrDr sqrtrM ?sqr_ge0// sqrtr_sqr.
+Qed.
+
+HB.instance Definition _ :=
+  PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (Rcomplex R) normcZ.
+
+Lemma Rcomplex_findim : Vector.axiom 2 (Rcomplex R).
+Proof.
+exists (fun x => \row_(i < 2) [:: Re x; Im x]`_i).
+  move=> r x y; apply/rowP; move=> i /=; rewrite !mxE.
+  case: i => i /=; rewrite ltnS leq_eqVlt => /orP[/eqP ->/=|].
+    by rewrite raddfD/= linearZ.
+  by rewrite ltnS leqn0 => /eqP -> /=; rewrite raddfD/= linearZ.
+apply: (@Bijective _ _ _ (fun x : 'rV_2 => x ord0 ord0 +i* x ord0 ord_max)).
+  by case=> x y; rewrite !mxE.
+move=> x; apply/rowP => i; rewrite mxE/=.
+case: i => i /[dup] + ilt; rewrite ltnS leq_eqVlt => /orP[/eqP /= i1|].
+  by rewrite {1}i1/=; congr (x ord0); apply: val_inj.
+rewrite ltnS leqn0 => /eqP i0/=.
+by rewrite {1}i0/=; congr (x ord0); apply: val_inj.
+Qed.
+
+HB.instance Definition _ :=
+  Lmodule_hasFinDim.Build R (Rcomplex R) Rcomplex_findim.
+
+End Rcomplex_NormedModType.
+End Rcomplex_NormedModType.
+
+Section Holomorphe_der.
+Variable R : realType.
+
+Local Notation sqrtr := Num.sqrt.
+Local Notation C := R[i].
+Local Notation Rc := (Rcomplex R).
+
+Definition holomorphic (f : C -> C) (c : C) :=
+  cvg ((fun h => h^-1 *: (f (c + h) - f c)) @ 0^').
+
+Lemma holomorphicP (f : C -> C) (c : C) : holomorphic f c <-> derivable f c 1.
+Proof.
+rewrite /holomorphic /derivable.
+suff ->: (fun h : C => h^-1 *: ((f (c + h) - f c))) =
+         ((fun h : C => h^-1 *: ((f \o shift c) (h *: 1) - f c))) by [].
+by apply: funext => h; rewrite complexA [X in f X]addrC.
+Qed.
+
+Definition Rdifferentiable (f : C -> C) (c : C) := differentiable f%:Rfun c%:Rc.
+
+Definition realC : R -> C := (fun r => r%:C).
+
+Lemma continuous_realC: continuous realC.
+Proof.
+move=> x A /= [] r /[dup] /realC_gt0 Rer0 /gt0_realC rRe H; exists (Re r) => //.
+by move=> z /= nz; apply: (H z%:C); rewrite /= -raddfB realC_norm rRe ltcR.
+Qed. 
+
+Lemma Rdiff1 (f : C -> C) c :
+  lim ((fun h : C => h^-1 *: ((f (c + h) - f c))) @ (realC @ 0^'))
+  = 'D_1 (f%:Rfun) c%:Rc.
+Proof.
+rewrite /derive.
+rewrite -[LHS]/(lim ((fun h : C => h^-1 *: ((f (c + h) - f c)))
+                  \o realC @ 0^')).
+suff ->: (fun h : C => h^-1 *: (f (c + h) - f c)) \o realC
+  = fun h : R => h^-1 *: ((f \o shift c) (h *: (1%:Rc)) - f c)%:Rc.
+  by [].
+apply: funext => h /=.
+by rewrite -fmorphV /= -!scalecr realC_alg [X in f X]addrC.
+Qed.
+
+Lemma Rdiffi (f : C -> C) c:
+  lim ((fun h : C => h^-1 *: ((f (c + h * 'i) - f c))) @ (realC @ 0^'))
+  = 'D_('i) (f%:Rfun) c%:Rc.
+Proof.
+rewrite /derive.
+rewrite -[LHS]/(lim ((fun h : (R[i]) => h^-1 *: (f (c + h * 'i) - f c))
+                  \o realC @ 0^')).
+suff -> : (fun h : (R[i]) => h^-1 * (f (c + h * 'i) - f c)) \o realC
+  = fun h : R => h^-1 *: ((f \o shift c) (h *: ('i%:Rc)) - f c)%:Rc.
+  by [].
+apply: funext => h /=.
+by rewrite -fmorphV -scalecE -!scalecr realCZ [X in f X]addrC.
+Qed.
+
+(* should be generalized to equivalent norms *)
+(* but there is no way to state it for now *)
+Lemma littleoCo (h e : C -> C) (x : C) :
+   [o_x (e : C -> C) of (h : C -> C)] =
+   [o_x (e : Rc -> Rc) of (h : Rc -> Rc)].
+Proof.
+suff heP : (h : C -> C) =o_x (e : C -> C) <->
+           (h : Rc -> Rc) =o_x (e : Rc -> Rc).
+  have [ho|hNo] := asboolP ((h : C -> C) =o_x (e : C -> C)).
+    by rewrite !littleoE// -!eqoP// -heP.
+  by rewrite !littleoE0// -!eqoP// -heP.
+rewrite !eqoP; split => small/= _ /posnumP[eps]; near=> y.
+  rewrite -lecR/= rmorphM/=.
+  near: y.
+  by apply: small; rewrite ltcR.
+rewrite -[_%:num]ger0_norm// -rmorphM/= lecR.
+by near: y; apply: small; rewrite (@normr_gt0 _ (Rcomplex R))//.
+Unshelve. all: by end_near. Qed.
+
+Definition CauchyRiemannEq (f : C -> C) c :=
+  'i * 'D_1 f%:Rfun c%:Rc = 'D_('i) f%:Rfun c%:Rc.
+
+Lemma holo_differentiable (f : C -> C) (c : C) :
+  holomorphic f c -> Rdifferentiable f c.
+Proof.
+move=> /holomorphicP /derivable1_diffP /diff_locallyP => -[cdiff holo].
+pose df : Rc -> Rc := 'd f c.
+have lDf : linear df by move=> t u v; rewrite /df !scalecr linearP.
+pose df' : {linear Rc -> Rc} :=
+  HB.pack df (GRing.isLinear.Build _ _ _ _ df lDf).
+apply/diff_locallyP; split; first exact: linear_findim_continuous.
+have eqdf : f%:Rfun \o +%R^~ c = cst (f c) + df' +o_ (0 : Rc) id.
+  rewrite [LHS]holo /df'/=/df/=.
+  congr (_ + _).
+  exact: littleoCo.
+rewrite (@diff_unique R (Rcomplex R) (Rcomplex R) _ df' _ _ eqdf).
+  exact: eqdf.
+exact: linear_findim_continuous.
+(* TODO: fix Qed performance issue (which is due to the proof of `eqdf`).
+  3.684s *)
+Qed.
+
+Lemma holo_CauchyRiemann (f : C -> C) c: holomorphic f c -> CauchyRiemannEq f c.
+Proof.
+move=> /cvg_ex; rewrite //= /CauchyRiemannEq. rewrite -Rdiff1 -Rdiffi.
+set quotC : C -> C := fun h : R[i] => h^-1 *: (f (c + h) - f c).
+set quotR : C -> C:= fun h => h^-1 *: (f (c + h * 'i) - f c) .
+move => /= [l H].
+have -> :  quotR @ (realC @ 0^') =  (quotR \o realC) @ 0^' by [].
+have realC'0:  realC @ 0^' --> 0^'.
+  rewrite -[0 in X in _ --> X]/(realC 0).
+  apply: within_continuous_withinNx; first by apply: continuous_realC.
+  by move => /= x /complexI.
+have HR0:(quotC \o (realC) @ 0^')  --> l.
+ by apply: cvg_comp; last by exact: H.
+have lem : quotC \o  *%R^~ 'i%R @ (realC @ (0 : R)^') --> l.
+  apply: cvg_comp; last by exact: H.
+  apply: (@cvg_comp _ _ _ realC ( *%R^~ 'i)); first by exact: realC'0.
+  rewrite -[0 in X in _ `=>` X](mul0r 'i%C).
+  apply: within_continuous_withinNx; first exact: scalel_continuous.
+  move=> x /eqP; rewrite mul0r mulIr_eq0; last by apply/rregP; apply: neq0Ci.
+  exact: eqP.
+have HRcomp: cvg (quotC \o *%R^~ 'i%R @ (realC @ ((0 : R)^'))) .
+  by apply/cvg_ex; simpl; exists l.
+have ->: lim (quotR @ (realC @ ((0 : R)^')))
+  = 'i *: lim (quotC \o ( fun h => h *'i) @ (realC @ ((0 : R)^'))).
+  have: 'i \*:quotC \o ( fun h => h *'i) =1 quotR.
+  move=> h /=; rewrite /quotC /quotR /=.
+  rewrite invfM scalerA mulrC -mulrA mulVf ?mulr1 ?neq0Ci //.
+  by move=> /funext <-; rewrite limZr.
+rewrite scalecE.
+suff ->: lim (quotC @ (realC @ ((0 : R)^')))
+      = lim (quotC \o  *%R^~ 'i%R @ (realC @ ((0 : R)^'))) by [].
+suff ->: lim (quotC @ (realC @ ((0 : R)^'))) = l.
+  by apply/eqP; rewrite eq_sym; apply/eqP; apply: (cvg_lim _ lem).
+by apply: cvg_lim; last exact: HR0.
+Qed.
+
+Lemma Diff_CR_holo (f : C -> C) (c : C):
+  (Rdifferentiable f c) /\ (CauchyRiemannEq f c) -> (holomorphic f c).
+Proof.
+move=> [] /= /[dup] H /diff_locallyP => [[derc diff]] CR.
+apply/holomorphicP/derivable1_diffP/diff_locallyP.
+pose Df := (fun h : C => h *: ('D_1 f%:Rfun c : C)).
+have lDf : linear Df by move=> t u v /=; rewrite /Df scalerDl scalerA scalecE.
+pose df : {linear R[i] -> R[i]} :=
+  HB.pack Df (GRing.isLinear.Build _ _ _ _ Df lDf).
+have cdf : continuous df by apply: scalel_continuous.
+have lem : Df = 'd (f%:Rfun) (c : Rc). (* issue with notation *)
+  apply: funext => z; rewrite  /Df.
+  set x := Re z; set y := Im z.
+  have zeq : z = x *: 1 %:Rc + y *: 'i%:Rc.
+  by rewrite [LHS]complexE /= realC_alg scalecr scalecE [in RHS]mulrC.
+  rewrite [X in 'd _ _ X]zeq addrC linearP linearZ /= -!deriveE //.
+  rewrite -CR (scalerAl y) -scalecE !scalecr /=.
+  rewrite -(scalerDl  (('D_1 f%:Rfun (c : Rc)) : C) _  (real_complex R x)).
+  by rewrite addrC -!scalecr -realC_alg -zeq.
+have holo:  f \o shift c = cst (f c) + df +o_ ( 0 : C) id.
+  rewrite [LHS]diff /= lem.
+  congr (_ + _).
+  exact/esym/littleoCo.
+by rewrite (diff_unique cdf holo).
+(* TODO: fix Qed performance issue (which is due to the proof of `holo`).
+  6.519s *)
+Qed.
+
+Lemma holomorphic_Rdiff (f : C -> C) (c : C) :
+  (Rdifferentiable f c) /\ (CauchyRiemannEq f c) <-> (holomorphic f c).
+Proof.
+split=> H; first exact: Diff_CR_holo.
+split; first exact: holo_differentiable.
+exact: holo_CauchyRiemann.
+Qed.
+
+End Holomorphe_der.
diff --git a/theories/landau.v b/theories/landau.v
index 2a2bd08aa..5846175d9 100644
--- a/theories/landau.v
+++ b/theories/landau.v
@@ -391,6 +391,11 @@ Lemma littleoE (tag : unit) (F : filter_on T)
    littleo_def F f h -> the_littleo tag F phF f h = f.
 Proof. by move=> /asboolP?; rewrite /the_littleo /insubd insubT. Qed.
 
+Lemma littleoE0 (tag : unit) (F : filter_on T)
+   (phF : phantom (set (set T)) F) f h :
+   ~ littleo_def F f h -> the_littleo tag F phF f h = 0.
+Proof. by move=> ?; rewrite /the_littleo /insubd insubN//; apply/asboolP. Qed.
+
 Canonical the_littleo_littleo (tag : unit) (F : filter_on T)
   (phF : phantom (set_system T) F) f h := [littleo of the_littleo tag F phF f h].
 
diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index edeccb19c..77ff6ccc6 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -20,6 +20,9 @@ From mathcomp Require Import ereal_normedtype pseudometric_normed_Zmodule.
 (*                normedModType K == interface type for a normed module       *)
 (*                                   structure over the numDomainType K       *)
 (*                                   The HB class is NormedModule.            *)
+(*               normedVectType K == interface type for a normed vectType     *)
+(*                                   structure over the numDomainType K       *)
+(*                                   The HB class is NormedVector.            *)
 (*                           `|x| == the norm of x (notation from ssrnum.v)   *)
 (* ```                                                                        *)
 (*                                                                            *)
@@ -140,6 +143,10 @@ HB.instance Definition _ :=
 
 HB.end.
 
+#[short(type="normedVectType")]
+HB.structure Definition NormedVector (K : numDomainType) :=
+  {T of NormedModule K T & Vector K T}.
+
 (**md see also `Section standard_topology_pseudoMetricNormedZmod` in
   `pseudometric_normed_Zmodule.v` *)
 Section standard_topology_normedMod.
@@ -334,6 +341,36 @@ Proof.
 by move=> k; apply: (cvg_comp2 cvg_id (cvg_cst _) (scale_continuous _ _ (_, _))).
 Qed.
 
+Lemma dnbhs0_le e :
+   0 < e -> \forall x \near (0 : V)^', `|x| <= e.
+Proof.
+move=> e_gt0; apply/nbhs_ballP; exists e => // x.
+rewrite -ball_normE /= sub0r normrN => le_nxe _ .
+by rewrite ltW.
+Qed.
+
+Lemma nbhs0_le e :
+   0 < e -> \forall x \near (0 : V)^', `|x| <= e.
+Proof.
+move=> e_gt0; apply/nbhs_ballP; exists e => // x.
+rewrite -ball_normE /= sub0r normrN => le_nxe _ .
+by rewrite ltW.
+Qed.
+
+Lemma dnbhs0_lt e :
+   0 < e -> \forall x \near (0 : V)^', `|x| < e.
+Proof.
+move=> e_gt0; apply/nbhs_ballP; exists e => // x.
+by rewrite -ball_normE /= sub0r normrN.
+Qed.
+
+Lemma nbhs0_lt e :
+   0 < e -> \forall x \near (0 : V)^', `|x| < e.
+Proof.
+move=> e_gt0; apply/nbhs_ballP; exists e => // x.
+by rewrite -ball_normE /= sub0r normrN.
+Qed.
+
 End NormedModule_numFieldType.
 Arguments cvg_at_rightE {K V} f x.
 Arguments cvg_at_leftE {K V} f x.
@@ -1961,3 +1998,282 @@ by rewrite interior_closed_ballE //; exact: ballxx.
 Qed.
 
 End Closed_Ball_normedModType.
+
+(* equip a normedZmodType with a structure of normed module *)
+
+Definition pseudometric (K : numFieldType) (M : normedZmodType K) : Type := M.
+
+HB.instance Definition _ (K : numFieldType) (M : normedZmodType K) :=
+  Choice.on (pseudometric M).
+HB.instance Definition _ (K : numFieldType) (M : normedZmodType K) :=
+  Num.NormedZmodule.on (pseudometric M).
+HB.instance Definition _ (K : numFieldType) (M : normedZmodType K) :=
+  isPointed.Build M 0.
+
+Section isnormedmodule.
+Variables (K : numFieldType) (M' : normedZmodType K).
+
+Notation M := (pseudometric M').
+
+Local Definition ball (x : M) (r : K) : set M := ball_ Num.norm x r.
+
+Local Definition ent : set_system (M * M) :=
+  entourage_ ball.
+
+Local Definition nbhs (x : M) : set_system M :=
+  nbhs_ ent x.
+
+Local Lemma nbhsE : nbhs = nbhs_ ent. Proof. by []. Qed.
+
+HB.instance Definition _ := hasNbhs.Build M nbhs.
+
+Local Lemma ball_center x (e : K) : 0 < e -> ball x e x.
+Proof. by rewrite /ball/= subrr normr0. Qed.
+
+Local Lemma ball_sym x y (e : K) : ball x e y -> ball y e x.
+Proof. by rewrite /ball /= distrC. Qed.
+
+Local Lemma ball_triangle x y z e1 e2 : ball x e1 y -> ball y e2 z ->
+  ball x (e1 + e2) z.
+Proof.
+rewrite /ball /= => ? ?.
+rewrite -[x](subrK y) -(addrA (x + _)).
+by rewrite (le_lt_trans (ler_normD _ _))// ltrD.
+Qed.
+
+Local Lemma entourageE : ent = entourage_ ball.
+Proof. by []. Qed.
+
+HB.instance Definition _ := @Nbhs_isPseudoMetric.Build K M
+  ent nbhsE ball ball_center ball_sym ball_triangle entourageE.
+
+End isnormedmodule.
+
+Section InfiniteNorm.
+Variables (R : numFieldType) (V : vectType R) (B : (\dim (@fullv _ V)).-tuple V).
+Let V' := @fullv _ V.
+Hypothesis (Bbasis : basis_of V' B).
+
+(* FIXME: Check naming. *)
+Definition oo_norm x := \big[Order.max/0]_(i < \dim V') `|coord B i x|.
+
+Definition oo_space : Type := (fun=> V) Bbasis.
+
+HB.instance Definition _ := Vector.on oo_space.
+
+HB.instance Definition _ := Pointed.copy oo_space V^o.
+
+Lemma oo_norm_ge0 x : 0 <= oo_norm x.
+Proof.
+rewrite /oo_norm.
+elim: (index_enum _) => /=; first by rewrite big_nil.
+by move=> i l IHl; rewrite big_cons /Order.max/=; case: ifP.
+Qed.
+
+Lemma le_coord_oo_norm x i : `|coord B i x| <= oo_norm x.
+Proof.
+rewrite /oo_norm; elim: (index_enum _) (mem_index_enum i) => //= j l IHl.
+rewrite inE big_cons /Order.max/= => /orP[/eqP <-|/IHl {}IHl]; case: ifP => [/ltW|]//.
+move=> /negP/negP.
+have bR: \big[Order.max/0]_(i <- l) `|coord B i x| \is Num.real.
+  exact: bigmax_real.
+move: (real_comparable bR (normr_real (coord B j x))).
+by move=> /comparable_leNgt <- /(le_trans IHl).
+Qed.
+
+Lemma ler_oo_normD x y : oo_norm (x + y) <= oo_norm x + oo_norm y.
+Proof.
+apply: bigmax_le => [|/= i _].
+  by apply: addr_ge0; apply: oo_norm_ge0.
+rewrite raddfD/=.
+by apply/(le_trans (ler_normD _ _))/lerD; apply: le_coord_oo_norm.
+Qed.
+
+Lemma oo_norm0_eq0 x : oo_norm x = 0 -> x = 0.
+Proof.
+move=> x0.
+rewrite (coord_basis Bbasis (memvf x)).
+suff: forall i, coord B i x = 0.
+  move=> {}x0.
+  under eq_bigr do rewrite x0.
+  by rewrite -scaler_sumr scale0r.
+move=> i; apply/normr0_eq0/le_anti/andP; split; last exact: normr_ge0.
+by rewrite -x0; apply: le_coord_oo_norm.
+Qed.
+
+Lemma oo_normZ r x : oo_norm (r *: x) = `|r| * oo_norm x.
+Proof.
+rewrite /oo_norm.
+under eq_bigr do rewrite linearZ normrZ/=.
+elim: (index_enum _) => [|i l IHl]; first by rewrite !big_nil mulr0.
+by rewrite !big_cons IHl maxr_pMr.
+Qed.
+
+Lemma oo_normMn x n : oo_norm (x *+ n) = oo_norm x *+ n.
+Proof. by rewrite -scaler_nat oo_normZ normr_nat mulr_natl. Qed.
+
+Lemma oo_normN x : oo_norm (- x) = oo_norm x.
+Proof. by rewrite -scaleN1r oo_normZ normrN1 mul1r. Qed.
+
+HB.instance Definition _ := Num.Zmodule_isNormed.Build R oo_space ler_oo_normD oo_norm0_eq0 oo_normMn oo_normN.
+
+HB.instance Definition _ := PseudoMetric.copy oo_space (pseudometric oo_space).
+
+HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R oo_space erefl.
+
+HB.instance Definition _ := PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R oo_space oo_normZ.
+
+End InfiniteNorm.
+
+Section EquivalenceNorms.
+Variables (R : realType) (V : vectType R).
+Let V' := @fullv _ V.
+Let Voo := oo_space (vbasisP (@fullv _ V)).
+
+(* N.B. Get Trocq to prove the continuity part automatically. *)
+Lemma oo_closed_ball_compact : compact (closed_ball (0 : Voo) 1).
+Proof.
+rewrite closed_ballE/closed_ball_//=.
+under eq_set do rewrite sub0r normrN.
+rewrite -[forall x, _]/(compact _).
+pose f (X : {ptws 'I_(\dim V') -> R^o}) : Voo := \sum_(i < \dim V') (X i) *: (vbasis V')`_i.
+have -> : [set x : Voo | `|x| <= 1] = f @` [set X | forall i, `[-1, 1]%classic (X i)].
+  apply/seteqP; split=> x/=.
+    move=> x1; exists (fun i => coord (vbasis V') i x); last first.
+      exact/esym/(@coord_vbasis _ _ (x : V))/memvf.
+    move=> i; rewrite in_itv/= -ler_norml.
+    apply: (le_trans _ x1).
+    exact: le_coord_oo_norm.
+  move=> [X] X1 <-.
+  rewrite /normr/=/oo_norm.
+  apply: bigmax_le => //= i _.
+  rewrite coord_sum_free; last exact/basis_free/vbasisP.
+  rewrite ler_norml.
+  exact: X1.
+apply: (@continuous_compact _ _ f); last first.
+  apply: (@tychonoff 'I_(\dim V') (fun=> R^o) (fun=> `[-1, 1 : R^o]%classic)).
+  move=> _.
+  exact: segment_compact.
+apply/continuous_subspaceT/sum_continuous => i _/= x.
+exact/continuousZl/proj_continuous. 
+Qed.
+
+Lemma equivalence_norms (N : V -> R) :
+  N 0 = 0 -> (forall x, 0 <= N x) -> (forall x, N x = 0 -> x = 0) -> (forall x y, N (x + y) <= N x + N y) ->
+  (forall r x, N (r *: x) = `|r| * N x) ->
+  exists M, 0 < M /\ forall x : Voo, `|x| <= M * N x /\ N x <= M * `|x|.
+Proof.
+move=> N0 N_ge0 N0_eq0 ND NZ.
+set M0 := 1 + \sum_(i < \dim V') N (vbasis V')`_i.
+have N_sum (I : Type) (r : seq I) (F : I -> V):
+  N (\sum_(i <- r) F i) <= \sum_(i <- r) N (F i).
+  elim: r => [|x r IHr]; first by rewrite !big_nil N0.
+  by rewrite !big_cons; apply/(le_trans (ND _ _))/lerD.
+have leNoo: forall x : Voo, N x <= M0 * `|x|.
+  move=> x.
+  rewrite [in leLHS](coord_vbasis (memvf (x : V))).
+  apply: (le_trans (N_sum _ _ _)).
+  rewrite mulrDl mul1r mulr_suml -[leLHS]add0r.
+  apply: lerD => //.
+  apply: ler_sum => /= i _.
+  rewrite NZ mulrC; apply: ler_pM => //.
+  exact: le_coord_oo_norm.
+have M00 : 0 < M0.
+  rewrite -[ltLHS]addr0.
+  by apply: ltr_leD => //; apply: sumr_ge0.
+have NC0 : continuous (N : Voo -> R).
+  move=> /= x.
+  rewrite /continuous_at.
+  apply: cvg_zero; first exact: nbhs_filter.
+  apply/cvgr0Pnorm_le; first exact: nbhs_filter.
+  move=> /= e e0.
+  near=> y.
+    rewrite -[_ y]/(N y - N x).
+    apply: (@le_trans _ _ (N (y - x))).
+      apply/real_ler_normlP.
+        by apply: realB; apply: ger0_real.
+      have NB a b : N a <= N b + N (a - b).
+        by rewrite -[a in N a]addr0 -(subrr b) addrCA ND.
+      rewrite opprB !lerBlDl; split; last exact: NB.
+      by rewrite -opprB -scaleN1r NZ normrN1 mul1r NB.
+    apply: (le_trans (leNoo _)).
+    rewrite mulrC -ler_pdivlMr// -opprB normrN.
+  near: y; apply: cvgr_dist_le; first exact: cvg_id.
+  exact: divr_gt0.
+have: compact [set x : Voo | `|x| = 1].
+  apply: (subclosed_compact  _ oo_closed_ball_compact); last first.
+    apply/subsetP => x.
+    rewrite closed_ballE// !inE/=.
+    by rewrite /closed_ball_/= sub0r normrN => ->.
+  apply: (@closed_comp _ _ _ [set 1 : R]); last exact: closed_eq.
+  by rewrite /prop_in1 => + _; apply: norm_continuous.
+move=> /(@continuous_compact _ _ (N : Voo -> R)) -/(_ _)/wrap[].
+  exact: continuous_subspaceT.
+move=> /(@continuous_compact _ _ (@GRing.inv R)) -/(_ _)/wrap[].
+  move=> /= x.
+  rewrite /continuous_at.
+  apply: (@continuous_in_subspaceT _ _ [set N x | x in [set x : Voo | `|x| = 1]] (@GRing.inv R)).
+  move=> r /set_mem/=[] y y1 <-.
+  apply: inv_continuous.
+  apply/negP => /eqP/N0_eq0 y0.
+  move: y1; rewrite y0 normr0 => /esym.
+  by move: (@oner_neq0 R) => /eqP.
+move=> /compact_bounded[] M1 [] M1R /(_ (1 + M1)).
+rewrite -subr_gt0 -addrA subrr addr0 => /(_ ltr01).
+rewrite /globally/= => M1N.
+exists (maxr M0 (1 + M1)).
+split=> [|x]; first by apply: (lt_le_trans M00); rewrite le_max lexx.
+split; last first.
+  apply/(le_trans (leNoo x))/ler_pM => //; first exact/ltW.
+  by rewrite /maxr; case: ifP => // /ltW.
+have [->|x0] := eqVneq x 0; first by rewrite normr0 N0 mulr0.
+have Nx0: 0 < N x.
+  rewrite lt0r N_ge0 andbT.
+  by move: x0; apply: contra => /eqP/N0_eq0/eqP.
+have normx0 : 0 < `|x|.
+  move: (lt_le_trans Nx0 (leNoo x)).
+  by rewrite pmulr_rgt0.
+move: M1N => /(_ (`|x| / N x)) -/(_ _)/wrap[].
+  exists (N x / `|x|); last by rewrite invf_div.
+  exists (`|x|^-1 *: x); last first.
+    by rewrite NZ mulrC ger0_norm.
+  rewrite normrZ mulrC ger0_norm.
+    by rewrite divrr//; apply: unitf_gt0.
+  by rewrite invr_ge0; apply: ltW.
+rewrite ger0_norm; last exact: divr_ge0.
+rewrite ler_pdivrMr// => xle.
+apply: (le_trans xle).
+rewrite -subr_ge0 -mulrBl pmulr_lge0// subr_ge0.
+by rewrite le_max lexx orbT.
+Unshelve. all: by end_near.
+Qed.
+
+End EquivalenceNorms.
+
+Section LinearContinuous.
+Variables (R : realType) (V : normedVectType R) (W : normedModType R).
+
+Lemma linear_findim_continuous (f : {linear V -> W}) : continuous f.
+Proof.
+set V' := @fullv _ V.
+set B := vbasis V' => /= x.
+rewrite /continuous_at.
+rewrite [x in f x](coord_vbasis (memvf x)) raddf_sum.
+rewrite (@eq_cvg _ _ _ _ (fun y => \sum_(i < \dim V') coord B i y *: f B`_i)); last first.
+  move=> y; rewrite [y in LHS](coord_vbasis (memvf y)) raddf_sum.
+  by apply: eq_big => // i _; apply: linearZ.
+apply: cvg_sum => i _.
+rewrite [X in _ --> X]linearZ/= -/B.
+apply: cvgZl.
+move: x; apply/linear_bounded_continuous/bounded_funP => r/=.
+have := @equivalence_norms R V (@normr R V) (@normr0 _ _) (@normr_ge0 _ _) (@normr0_eq0 _ _) (@ler_normD _ _) (@normrZ _ _).
+move=> [] M [] M0 MP.
+exists (M * r) => x.
+move: MP => /(_ x)[] Mx Mx' xr.
+apply/(le_trans (le_coord_oo_norm _ _ _))/(le_trans Mx).
+rewrite -subr_ge0 -mulrBr; apply: mulr_ge0; first exact: ltW.
+by rewrite subr_ge0. 
+Qed.
+
+End LinearContinuous.
+
diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v
index 7a213364c..1ce675f1d 100644
--- a/theories/topology_theory/num_topology.v
+++ b/theories/topology_theory/num_topology.v
@@ -83,6 +83,10 @@ HB.instance Definition _ (R : numFieldType) :=
   Uniform_isPseudoMetric.Build R R^o
     ball_norm_center ball_norm_symmetric ball_norm_triangle erefl.
 
+HB.instance Definition _ (R : numFieldType) :=
+  Uniform_isPseudoMetric.Build R R^o
+    ball_norm_center ball_norm_symmetric ball_norm_triangle erefl.
+
 Lemma real_order_nbhsE (R : realFieldType) (x : R^o) : nbhs x =
   filter_from (fun i => itv_open_ends i /\ x \in i) (fun i => [set` i]).
 Proof.
diff --git a/theories/topology_theory/uniform_structure.v b/theories/topology_theory/uniform_structure.v
index 611643c7d..7e8a9fdbc 100644
--- a/theories/topology_theory/uniform_structure.v
+++ b/theories/topology_theory/uniform_structure.v
@@ -284,6 +284,26 @@ rewrite !near_simpl near_withinE near_simpl => Pf; near=> y.
 by have [->|] := eqVneq y x; [by apply: nbhs_singleton|near: y].
 Unshelve. all: by end_near. Qed.
 
+Lemma within_continuous_withinNx
+  (T U : topologicalType) (f : T -> U) (x : T) :
+  {for x, continuous f} ->
+  (forall y, f y = f x -> y = x) -> f @ x^' --> (f x)^'.
+Proof.
+move=> cf fI A.
+rewrite /nbhs /= /dnbhs !withinE/= => -[] V Vfx AV.
+move: (cf _ Vfx); rewrite /nbhs/= -/(nbhs _ _) => Vx.
+exists (f @^-1` V) => //.
+apply/seteqP; split=> y/= [] fyAV yx; split=> //.
+  suff: f y \in A `&` (fun y : U => y != f x).
+    by rewrite AV inE => -[].
+  rewrite inE/=; split=> //.
+  by move: yx; apply: contra => /eqP /fI /eqP.
+suff: f y \in V `&` (fun y : U => y != f x).
+  by rewrite -AV inE => -[].
+rewrite inE/=; split=> //.
+by move: yx; apply: contra => /eqP /fI /eqP.
+Qed.
+
 (* This property is primarily useful for metrizability on uniform spaces *)
 Definition countable_uniformity (T : uniformType) :=
   exists R : set_system (T * T), [/\
diff --git a/theories/tvs.v b/theories/tvs.v
index fe4359304..045240c71 100644
--- a/theories/tvs.v
+++ b/theories/tvs.v
@@ -90,6 +90,22 @@ HB.mixin Record PreTopologicalNmodule_isTopologicalNmodule M
 HB.structure Definition TopologicalNmodule :=
   {M of PreTopologicalNmodule M & PreTopologicalNmodule_isTopologicalNmodule M}.
 
+Section TopologicalNmodule_Theory.
+
+Lemma cvg_sum (T : Type) (U : TopologicalNmodule.type) (F : set_system T)
+  (I : Type) (r : seq I) (P : pred I) (Ff : I -> T -> U) (Fa : I -> U) :
+  Filter F -> (forall i, P i -> Ff i x @[x --> F] --> Fa i) ->
+  \sum_(i <- r | P i) Ff i x @[x --> F] --> \sum_(i <- r| P i) Fa i.
+Proof. by move=> FF Ffa; apply: cvg_big => //; apply: add_continuous. Qed.
+
+Lemma sum_continuous (T : topologicalType) (M : TopologicalNmodule.type) 
+  (I : Type) (r : seq I) (P : pred I) (F : I -> T -> M) :
+  (forall i : I, P i -> continuous (F i)) ->
+  continuous (fun x1 : T => \sum_(i <- r | P i) F i x1).
+Proof. by move=> FC0; apply: continuous_big => //; apply: add_continuous. Qed.
+
+End TopologicalNmodule_Theory.
+
 HB.structure Definition PreTopologicalZmodule :=
   {M of Topological M & GRing.Zmodule M}.
 
@@ -273,6 +289,27 @@ exists (U1, ((fun xy : M * M => (- xy.1, - xy.2)) @^-1` U2)); first by split.
 by move=> /= [] [] a1 a2 [] b1 b2/= [] aU bU; exists (a1, b1, (a2, b2)).
 Qed.
 
+Lemma entourage_nbhsE : @entourage M = filter_from (nbhs 0) (fun X => [set x | x.2 - x.1 \in X]).
+Proof.
+have map_uniform (T U : uniformType) (S : set (U * U)%type) (f : T * T -> U) : unif_continuous f -> entourage S -> exists ST : set (T * T)%type, entourage ST /\ {in ST, forall x, forall y, (f (x.1, y), f (x.2, y)) \in S}.
+  move=> fu /fu [[]]/= ST1 ST2 [] ? ? /subsetP STf.
+  exists ST1; split=> // x xST1 y.
+  have /STf: (x, (y, y)) \in ST1 `*` ST2.
+    rewrite in_setX xST1/= unfold_in/=.
+    apply/asboolT.
+    exact: entourage_refl.
+  rewrite in_setE/= => -[] [] [] a1 a2 [] b1 b2 /= abS [] <- {2}<- <-/=.
+  exact: asboolT.
+rewrite eqEsubset; split; apply/subsetP => U; rewrite !inE /filter_from/=.
+  move=> /(map_uniform _ _ _ _ sub_unif_continuous)/= [] V [] Ve VU.
+  exists (xsection V 0); first exact: nbhs_entourage.
+  apply/subsetP => [] [] x y; rewrite inE/= mem_xsection => /VU/(_ (-x))/=.
+  by rewrite opprK -addrA addNr add0r addr0.
+move=> [] V /nbhsP[] U' /(map_uniform _ _ _ _ add_unif_continuous)/= [] W [] We WU' /subsetP U'V /subsetP VU.
+apply/(filterS _ We)/subsetP => -[] a b /WU'/=/(_ (-a)); rewrite subrr => abU'.
+by apply/VU; rewrite inE/=; apply: U'V; rewrite mem_xsection.
+Qed.
+
 End UniformZmoduleTheory.
 
 HB.structure Definition PreUniformLmodule (K : numDomainType) :=
@@ -514,6 +551,16 @@ rewrite /ball /ball_/= => xy /= [nx ny].
 by rewrite opprD addrACA (le_lt_trans (ler_normD _ _)) // (splitr e) ltrD.
 Qed.
 
+Local Lemma standard_sub_unif_continuous : unif_continuous (fun x : R^o * R^o => x.1 - x.2).
+Proof.
+move=> /= U; rewrite /nbhs/= -!entourage_ballE => -[]/= e e0 /subsetP eU.
+exists (e / 2) => /=; first exact: divr_gt0.
+apply/subsetP => -[] [] a1 a2 [] b1 b2/=; rewrite inE/= => -[]/=.
+rewrite /ball/= => abe1 abe2.
+apply: eU => /=; rewrite inE/= /ball/= opprD addrACA -opprD.
+by rewrite (le_lt_trans (ler_normB _ _))// (splitr e) ltrD.
+Qed.
+
 Local Lemma standard_scale_continuous : continuous (fun z : R^o * R^o => z.1 *: z.2).
 Proof.
 (* NB: This lemma is proved once again in normedtype, in a shorter way with much more machinery *)
@@ -591,6 +638,7 @@ Qed.
 
 HB.instance Definition _ :=
   PreTopologicalNmodule_isTopologicalNmodule.Build R^o standard_add_continuous.
+HB.instance Definition _ := PreUniformNmodule_isUniformZmodule.Build R^o standard_sub_unif_continuous.
 HB.instance Definition _ :=
   TopologicalNmodule_isTopologicalLmodule.Build R R^o standard_scale_continuous.
 HB.instance Definition _ := Uniform_isTvs.Build R R^o standard_locally_convex.