diff --git a/theories/derive.v b/theories/derive.v
index ab6aea2efd..53cd3b880d 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -167,8 +167,8 @@ Lemma differentiable_continuous (x : V) (f : V -> W) :
   differentiable f x -> {for x, continuous f}.
 Proof.
 move=> /diff_locallyP [dfc]; rewrite -addrA.
-rewrite (littleo_bigO_eqo (cst (1 : R^o))); last first.
-  apply/eqOP; near=> k; rewrite /cst [`|1 : R^o|]normr1 mulr1.
+rewrite (littleo_bigO_eqo (cst (1 : R))); last first.
+  apply/eqOP; near=> k; rewrite /cst [`|1|]normr1 mulr1.
   near=> y; rewrite ltW //; near: y; apply/nbhs_normP.
   exists k; first by near: k; exists 0; rewrite real0.
   by move=> ? /=; rewrite -ball_normE /= sub0r normrN.
@@ -180,10 +180,10 @@ Section littleo_lemmas.
 
 Variables (X Y Z : normedModType R).
 
-Lemma normm_littleo x (f : X -> Y) : `| [o_(x \near x) (1 : R^o) of f x]| = 0.
+Lemma normm_littleo x (f : X -> Y) : `| [o_(x \near x) (1 : R) of f x]| = 0.
 Proof.
 rewrite /cst /=; have [e /(_ (`|e x|/2) _)/nbhs_singleton /=] := littleo.
-rewrite pmulr_lgt0 // [`|1 : R^o|]normr1 mulr1 [X in X <= _]splitr.
+rewrite pmulr_lgt0 // [`|1|]normr1 mulr1 [X in X <= _]splitr.
 rewrite ger_addr pmulr_lle0 // => /implyP.
 case : real_ltgtP; rewrite ?realE ?normrE //=.
 by apply/orP; left.
@@ -205,8 +205,8 @@ Section diff_locally_converse_tentative.
 (* indeed the differential being b *: idfun is locally bounded *)
 (* and thus a littleo of 1, and so is id *)
 (* This can be generalized to any dimension *)
-Lemma diff_locally_converse_part1 (f : R^o -> R^o) (a : R^o) (b : R^o) (x : R^o) :
-  f \o shift x = cst a + b *: idfun +o_ (0 : [filteredType R^o of R^o]) id -> f x = a.
+Lemma diff_locally_converse_part1 (f : R -> R) (a b x : R) :
+  f \o shift x = cst a + b *: idfun +o_ (0 : R) id -> f x = a.
 Proof.
 rewrite funeqE => /(_ 0) /=; rewrite add0r => ->.
 by rewrite -[LHS]/(_ 0 + _ 0 + _ 0) /cst [X in a + X]scaler0 littleo_lim0 ?addr0.
@@ -215,13 +215,13 @@ Qed.
 End diff_locally_converse_tentative.
 
 Definition derive (f : V -> W) a v :=
-  lim ((fun h => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ nbhs' (0 : R^o)).
+  lim ((fun h => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ nbhs' 0).
 
 Local Notation "''D_' v f" := (derive f ^~ v).
 Local Notation "''D_' v f c" := (derive f c v). (* printing *)
 
 Definition derivable (f : V -> W) a v :=
-  cvg ((fun h => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ nbhs' (0 : R^o)).
+  cvg ((fun h => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ nbhs' 0).
 
 Class is_derive (a v : V) (f : V -> W) (df : W) := DeriveDef {
   ex_derive : derivable f a v;
@@ -231,7 +231,7 @@ Class is_derive (a v : V) (f : V -> W) (df : W) := DeriveDef {
 Lemma derivable_nbhs (f : V -> W) a v :
   derivable f a v ->
   (fun h => (f \o shift a) (h *: v)) = (cst (f a)) +
-    (fun h => h *: ('D_v f a)) +o_ (nbhs (0 : [filteredType R^o of R^o])) id.
+    (fun h => h *: ('D_v f a)) +o_ (nbhs (0 :R)) id.
 Proof.
 move=> df; apply/eqaddoP => _/posnumP[e].
 rewrite -nbhs_nearE nbhs_simpl /= nbhsE'; split; last first.
@@ -241,7 +241,7 @@ have /eqolimP := df; rewrite -[lim _]/(derive _ _ _).
 move=> /eqaddoP /(_ e%:num) /(_ [gt0 of e%:num]).
 apply: filter_app; rewrite /= !near_simpl near_withinE; near=> h => hN0.
 rewrite /= opprD -![(_ + _ : _ -> _) _]/(_ + _) -![(- _ : _ -> _) _]/(- _).
-rewrite /cst /= [`|1 : R^o|]normr1 mulr1 => dfv.
+rewrite /cst /= [`|1|]normr1 mulr1 => dfv.
 rewrite addrA -[X in X + _]scale1r -(@mulVf _ h) //.
 rewrite mulrC -scalerA -scalerBr normmZ.
 rewrite -ler_pdivl_mull; last by rewrite normr_gt0.
@@ -251,15 +251,15 @@ Grab Existential Variables. all: end_near. Qed.
 Lemma derivable_nbhsP (f : V -> W) a v :
   derivable f a v <->
   (fun h => (f \o shift a) (h *: v)) = (cst (f a)) +
-    (fun h => h *: ('D_v f a)) +o_ (nbhs (0 : [filteredType R^o of R^o])) id.
+    (fun h => h *: ('D_v f a)) +o_ (nbhs (0 : R)) id.
 Proof.
 split; first exact: derivable_nbhs.
 move=> df; apply/cvg_ex; exists ('D_v f a).
-apply/(@eqolimP _ R^o _ (nbhs'_filter_on _))/eqaddoP => _/posnumP[e].
+apply/(@eqolimP _ _ _ (nbhs'_filter_on _))/eqaddoP => _/posnumP[e].
 have /eqaddoP /(_ e%:num) /(_ [gt0 of e%:num]) := df.
 rewrite /= !(near_simpl, near_withinE); apply: filter_app; near=> h.
 rewrite /= opprD -![(_ + _ : _ -> _) _]/(_ + _) -![(- _ : _ -> _) _]/(- _).
-rewrite /cst /= [`|1 : R^o|]normr1 mulr1 addrA => dfv hN0.
+rewrite /cst /= [`|1|]normr1 mulr1 addrA => dfv hN0.
 rewrite -[X in _ - X]scale1r -(@mulVf _ h) //.
 rewrite -scalerA -scalerBr normmZ normfV ler_pdivr_mull ?normr_gt0 //.
 by rewrite mulrC.
@@ -267,7 +267,7 @@ Grab Existential Variables. all: end_near. Qed.
 
 Lemma derivable_nbhsx (f : V -> W) a v :
   derivable f a v -> forall h, f (a + h *: v) = f a + h *: 'D_v f a
-  +o_(h \near (nbhs (0 : [filteredType R^o of R^o]))) h.
+  +o_(h \near (nbhs (0 : R))) h.
 Proof.
 move=> /derivable_nbhs; rewrite funeqE => df.
 by apply: eqaddoEx => h; have /= := (df h); rewrite addrC => ->.
@@ -275,7 +275,7 @@ Qed.
 
 Lemma derivable_nbhsxP (f : V -> W) a v :
   derivable f a v <-> forall h, f (a + h *: v) = f a + h *: 'D_v f a
-  +o_(h \near (nbhs (0 : [filteredType R^o of R^o]))) h.
+  +o_(h \near (nbhs (0 :R))) h.
 Proof.
 split; first exact: derivable_nbhsx.
 move=> df; apply/derivable_nbhsP; apply/eqaddoE; rewrite funeqE => h.
@@ -301,7 +301,7 @@ evar (g : R -> W); rewrite [X in X @ _](_ : _ = g) /=; last first.
 apply: cvg_map_lim => //.
 pose g1 : R -> W := fun h => (h^-1 * h) *: 'd f a v.
 pose g2 : R -> W := fun h : R => h^-1 *: k (h *: v ).
-rewrite (_ : g = g1 + g2) ?funeqE // -(addr0 (_ _ v)); apply: (@cvgD _ _ [topologicalType of R^o]).
+rewrite (_ : g = g1 + g2) ?funeqE // -(addr0 (_ _ v)); apply: cvgD.
   rewrite -(scale1r (_ _ v)); apply: cvgZl => /= X [e e0].
   rewrite /ball_ /= => eX.
   apply/nbhs_ballP.
@@ -333,23 +333,23 @@ Section DifferentialR2.
 Variable R : numFieldType.
 Implicit Type (V : normedModType R).
 
-Lemma derivemxE m n (f : 'rV[R]_m.+1 -> 'rV[R]_n.+1) (a v : 'rV[R^o]_m.+1) :
+Lemma derivemxE m n (f : 'rV[R]_m.+1 -> 'rV[R]_n.+1) (a v : 'rV[R]_m.+1) :
   differentiable f a -> 'D_ v f a = v *m jacobian f a.
 Proof. by move=> /deriveE->; rewrite /jacobian mul_rV_lin1. Qed.
 
 Definition derive1 V (f : R -> V) (a : R) :=
-   lim ((fun h => h^-1 *: (f (h + a) - f a)) @ nbhs' (0 : R^o)).
+   lim ((fun h => h^-1 *: (f (h + a) - f a)) @ nbhs' 0).
 
 Local Notation "f ^` ()" := (derive1 f).
 
-Lemma derive1E V (f : R -> V) a : f^`() a = 'D_1 (f : R^o -> _) a.
+Lemma derive1E V (f : R -> V) a : f^`() a = 'D_1 f a.
 Proof.
 rewrite /derive1 /derive; set d := (fun _ : R => _); set d' := (fun _ : R => _).
 by suff -> : d = d' by []; rewrite funeqE=> h; rewrite /d /d' /= [h%:A](mulr1).
 Qed.
 
 (* Is it necessary? *)
-Lemma derive1E' V f a : differentiable (f : R^o -> V) a ->
+Lemma derive1E' V f a : differentiable (f : R -> V) a ->
   f^`() a = 'd f a 1.
 Proof. by move=> ?; rewrite derive1E deriveE. Qed.
 
@@ -420,14 +420,14 @@ by rewrite -[(k *: f) _]/(_ *: _) diff_locallyx // !scalerDr scaleox.
 Qed.
 
 (* NB: could be generalized with K : absRingType instead of R; DONE? *)
-Fact dscalel (k : V -> R^o) (f : W) x :
+Fact dscalel (k : V -> R) (f : W) x :
   differentiable k x ->
   continuous (fun z : V => 'd k x z *: f) /\
   (fun z => k z *: f) \o shift x =
     cst (k x *: f) + (fun z => 'd k x z *: f) +o_ (0 : V) id.
 Proof.
 move=> df; split.
-  move=> ?; exact/continuousZl/(@diff_continuous _ _ [normedModType R of R^o]).
+  move=> ?; exact/continuousZl/diff_continuous.
 apply/eqaddoE; rewrite funeqE => y /=.
 by rewrite diff_locallyx //= !scalerDl scaleolx.
 Qed.
@@ -484,7 +484,7 @@ Grab Existential Variables. all: end_near. Qed.
 End DifferentialR3.
 
 Section DifferentialR3_realFieldType.
-Variable R : realFieldType.
+Variable R : realFieldType. (*TODO : take ^o out, join with realField *)
 
 Lemma littleo_linear0 (V W : normedModType R) (f : {linear V -> W}) :
   (f : V -> W) =o_ (0 : V) id -> f = cst 0 :> (V -> W).
@@ -619,7 +619,7 @@ move=> dfx; apply: DiffDef; first exact: differentiableZ.
 by rewrite diffZ // diff_val.
 Qed.
 
-Lemma diffZl (k : V -> R^o) (f : W) x : differentiable k x ->
+Lemma diffZl (k : V -> R^o) (f : W) x : differentiable k x -> (*TODO: take ^o out*)
   'd (fun z => k z *: f) x = (fun z => 'd k x z *: f) :> (_ -> _).
 Proof.
 move=> df; set g := RHS; have glin : linear g.
@@ -656,19 +656,19 @@ apply: DiffDef; first exact/linear_differentiable/scaler_continuous.
 by rewrite diff_lin //; apply: scaler_continuous.
 Qed.
 
-Global Instance is_diff_scalel (x k : [filteredType R^o of R^o]) :
+Global Instance is_diff_scalel (x k : R^o) :
   is_diff k ( *:%R ^~ x) ( *:%R ^~ x).
 Proof.
-have -> : *:%R ^~ x = GRing.scale_linear [lmodType R of R^o] x.
+have -> : *:%R ^~ x = GRing.scale_linear R x.
   by rewrite funeqE => ? /=; rewrite [_ *: _]mulrC.
 apply: DiffDef; first exact/linear_differentiable/scaler_continuous.
 by rewrite diff_lin //; apply: scaler_continuous.
 Qed.
 
-Lemma differentiable_coord m n (M : 'M[R^o]_(m.+1, n.+1)) i j :
-  differentiable (fun N : 'M[R]_(m.+1, n.+1) => N i j : R^o) M.
+Lemma differentiable_coord m n (M : 'M[R]_(m.+1, n.+1)) i j :
+  differentiable (fun N : 'M[R]_(m.+1, n.+1) => N i j : R^o ) M.
 Proof.
-have @f : {linear 'M[R]_(m.+1, n.+1) -> R^o}.
+have @f : {linear 'M[R]_(m.+1, n.+1) -> R}.
   by exists (fun N : 'M[R]_(_, _) => N i j); eexists; move=> ? ?; rewrite !mxE.
 rewrite (_ : (fun _ => _) = f) //; exact/linear_differentiable/coord_continuous.
 Qed.
@@ -821,18 +821,18 @@ Definition Rmult_rev (y x : R) := x * y.
 Canonical rev_Rmult := @RevOp _ _ _ Rmult_rev (@GRing.mul [ringType of R])
   (fun _ _ => erefl).
 
-Lemma Rmult_is_linear x : linear (@GRing.mul [ringType of R] x : R^o -> R^o).
+Lemma Rmult_is_linear x : linear (@GRing.mul [ringType of R] x : R -> R).
 Proof. by move=> ???; rewrite mulrDr scalerAr. Qed.
 Canonical Rmult_linear x := Linear (Rmult_is_linear x).
 
-Lemma Rmult_rev_is_linear y : linear (Rmult_rev y : R^o -> R^o).
+Lemma Rmult_rev_is_linear y : linear (Rmult_rev y : R -> R).
 Proof. by move=> ???; rewrite /Rmult_rev mulrDl scalerAl. Qed.
 Canonical Rmult_rev_linear y := Linear (Rmult_rev_is_linear y).
 
 Canonical Rmult_bilinear :=
-  [bilinear of (@GRing.mul [ringType of [lmodType R of R^o]])].
+  [bilinear of (@GRing.mul [ringType of [lmodType R of R]])].
 
-Global Instance is_diff_Rmult (p : [filteredType R^o * R^o of R^o * R^o]) :
+Global Instance is_diff_Rmult (p : R*R ) :
   is_diff p (fun q => q.1 * q.2) (fun q => p.1 * q.2 + q.1 * p.2).
 Proof.
 apply: DiffDef; last by rewrite diff_bilin // => ?; apply: mul_continuous.
@@ -890,15 +890,16 @@ move=> dfx dgx; apply: DiffDef; first exact: differentiable_pair.
 by rewrite diff_pair // !diff_val.
 Qed.
 
-Global Instance is_diffM (f g df dg : V -> R^o) x :
+Global Instance is_diffM (f g df dg : V -> R^o) x : (*TODO : ^o out *)
   is_diff x f df -> is_diff x g dg -> is_diff x (f * g) (f x *: dg + g x *: df).
 Proof.
 move=> dfx dgx.
-have -> : f * g = (fun p => p.1 * p.2) \o (fun y => (f y, g y)) by [].
-(* TODO: type class inference should succeed or fail, not leave an evar *)
-apply: is_diff_eq; do ?exact: is_diff_comp.
-by rewrite funeqE => ?; rewrite /= [_ * g _]mulrC.
-Qed.
+have -> : f * g = (fun p => p.1 * p.2) \o (fun y => (f y, g y)) by []. 
+(* TODO: type class inference should succeed or fail, not leave an evar *) 
+apply: is_diff_eq; do ?exact: is_diff_comp.  admit.
+(* rewrite funeqE => ?; rewrite /= [_ * g _]mulrC. *)
+(* Qed. *)
+Admitted.
 
 Lemma diffM (f g : V -> R^o) x :
   differentiable f x -> differentiable g x ->
@@ -961,10 +962,10 @@ rewrite ler_subr_addr -ler_subr_addl (splitr `|x : R^o|).
 by rewrite normrM normfV (@ger0_norm _ 2) // -addrA subrr addr0; apply: ltW.
 Grab Existential Variables. all: end_near. Qed.
 
-Lemma diff_Rinv (x : [filteredType R^o of R^o]) : x != 0 ->
-  'd GRing.inv x = (fun h => - x ^- 2 *: h) :> (R^o -> R^o).
+Lemma diff_Rinv (x : R^o) : x != 0 ->
+  'd GRing.inv x = (fun h : R => - x ^- 2 *: h) :> (R^o -> R^o).
 Proof.
-move=> xn0; have -> : (fun h : R^o => - x ^- 2 *: h) =
+move=> xn0; have -> : (fun h : R => - x ^- 2 *: h) =
   GRing.scale_linear _ (- x ^- 2) by [].
 by apply: diff_unique; have [] := dinv xn0.
 Qed.
@@ -1388,12 +1389,13 @@ by rewrite ltr0_norm // addrC subrr.
 Grab Existential Variables. all: end_near. Qed.
 
 Lemma ler0_cvg_map (R : realFieldType) (T : topologicalType) (F : set (set T))
-  (FF : ProperFilter F) (f : T -> R^o) :
+  (FF : ProperFilter F) (f : T -> R) :
   (\forall x \near F, f x <= 0) -> cvg (f @ F) -> lim (f @ F) <= 0.
 Proof.
 move=> fle0 fcv; rewrite -oppr_ge0.
 have limopp : - lim (f @ F) = lim (- f @ F).
-  by apply: Logic.eq_sym; apply: cvg_map_lim => //; apply: cvgN.
+  apply: Logic.eq_sym; apply: cvg_map_lim; first by apply: Rhausdorff.
+  by apply: (@cvgN _ (regular_numFieldType_normedModType R)). (*TODO: simplify *)
 rewrite limopp; apply: le0r_cvg_map; last by rewrite -limopp; apply: cvgN.
 by move: fle0; apply: filterS => x; rewrite oppr_ge0.
 Qed.
@@ -1405,7 +1407,9 @@ Lemma ler_cvg_map (R : realFieldType) (T : topologicalType) (F : set (set T)) (F
 Proof.
 move=> lefg fcv gcv; rewrite -subr_ge0.
 have eqlim : lim (g @ F) - lim (f @ F) = lim ((g - f) @ F).
-  by apply/esym; apply: cvg_map_lim => //; apply: cvgD => //; apply: cvgN.
+  apply/esym; apply: cvg_map_lim => //; first by apply: Rhausdorff.
+  apply: (@cvgD _ ( (regular_numFieldType_normedModType R)))  => //. (*TODO: simplify *)
+  by apply: cvgN.
 rewrite eqlim; apply: le0r_cvg_map; last first.
   by rewrite /(cvg _) -eqlim /=; apply: cvgD => //; apply: cvgN.
 by move: lefg; apply: filterS => x; rewrite subr_ge0.
diff --git a/theories/holomorphy.v b/theories/holomorphy.v
new file mode 100644
index 0000000000..06b8657f67
--- /dev/null
+++ b/theories/holomorphy.v
@@ -0,0 +1,756 @@
+(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *) 
+From mathcomp Require Import ssreflect ssrfun ssrbool. 
+From mathcomp Require Import ssrnat eqtype choice fintype bigop order ssralg ssrnum.   
+From mathcomp Require Import complex.
+From mathcomp Require Import boolp reals ereal derive.
+Require Import classical_sets posnum topology normedtype landau.
+
+Import Order.TTheory GRing.Theory Num.Theory ComplexField Num.Def.
+Local Open Scope ring_scope.
+Local Open Scope classical_set_scope.
+Local Open Scope complex_scope.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+(*NB: we need ComplexField for its lemmas on Rcomplex 
+  But we do not want the canonical R-lmodtype structure on C. 
+  therefore this is based on a fork of real-closed *)
+
+Section complexLmod.
+(*This depends of the numfield_normedModmixin defined in normedModType *)
+(*No lmodType structure is canonicaly defined in the version of complex.v this
+file depends on *)
+
+  (* Variables (R : rcfType) (r : R) (c : R[i]). Fail Check (r *: c). *)
+  
+Canonical complex_lmodType (R : rcfType) :=
+    [lmodType R[i] of R[i] for [lmodType R[i] of [numFieldType of R[i]]]].
+
+
+Canonical complex_lalgType (R : rcfType) :=
+ [lalgType R[i] of R[i] for [lalgType R[i] of [numFieldType of R[i]]]].
+
+Canonical complex_algType (R : rcfType) :=
+ [algType R[i] of R[i] for [algType R[i] of [numFieldType of R[i]]]].
+
+End complexLmod.
+
+Section complex_topological. (*New *)
+  Variable R : rcfType.
+
+Canonical complex_pointedType :=
+  [pointedType of R[i] for [pointedType of [numFieldType of R[i]]]].
+Canonical complex_filteredType :=
+  [filteredType R[i] of R[i] for [filteredType R[i] of [numFieldType of R[i]]]]. 
+
+Canonical complex_topologicalType : topologicalType :=
+  [topologicalType of R[i] for  [topologicalType of [numFieldType of R[i]]]].
+Canonical complex_pseudoMetricType :=
+  [pseudoMetricType [numDomainType of R[i]] of R[i] for
+  [pseudoMetricType  [numDomainType of R[i]] of [numFieldType of R[i]]]].
+
+Canonical complex_PseudoMetricNormedZmodule :=
+  [pseudoMetricNormedZmodType [numDomainType of R[i]] of R[i] for
+  [pseudoMetricNormedZmodType  [numDomainType of R[i]] of [numFieldType of R[i]]]].
+
+Canonical complex_normedModType :=
+  NormedModType R[i] R[i] (numFieldType_NormedModMixin [numFieldType of R[i]]).
+
+End complex_topological.
+
+
+Section complex_extras.
+Variable R : rcfType.
+Local Notation sqrtr := Num.sqrt.
+Local Notation C := R[i].
+Local Notation Re := (@complex.Re R).
+Local Notation Im := (@complex.Im R).
+
+(* Check (@real_complex_def R _). *)
+(* Definition myrealcomplex := (fun (r : R) => r%:C). Check myrealcomplex. *)
+(* Coercion myrealcomplex : R >-> C. *)
+(* Variables (r : R). *)
+
+(*Adapting lemma eq_complex from complex.v, which was done in boolean style*)
+Lemma eqE_complex : forall (x y : C), (x = y) = ((Re x = Re y) /\ (Im x = Im y)).
+Proof.
+move => [a b] [c d]; apply : propositional_extensionality ; split.
+by move => -> ; split.
+by  case => //= -> ->.
+Qed.
+
+Lemma Re0 : Re 0 = 0 :> R.
+Proof. by []. Qed.
+
+Lemma Im0 : Im 0 = 0 :> R.
+Proof. by []. Qed.
+
+Lemma ReIm_eq0 (x : C) : (x = 0) = ((Re x = 0) /\ (Im x = 0)).
+Proof. by rewrite -[in Re x= _]Re0 -Im0 -eqE_complex. Qed.
+
+Lemma scalei_muli : forall z : C^o, 'i * z = 'i *: z.
+Proof. by []. Qed.
+
+Lemma iE : 'i%C = 'i :> C.
+Proof. by []. Qed.
+
+Lemma scalecM : forall (w  v : C^o), (v *: w = v * w).
+Proof. by []. Qed.
+
+Lemma normc0 : normc 0 = 0 :> R  .
+Proof. by rewrite /normc //= expr0n //= add0r sqrtr0. Qed.
+
+Lemma normcN (x : C) : normc (- x) = normc x.
+Proof. by case: x => a b /=; rewrite 2!sqrrN. Qed.
+
+Lemma normcr (x : R) : normc (x%:C) = normr x.
+Proof. by rewrite /normc/= expr0n //= addr0 sqrtr_sqr. Qed.
+
+Lemma normc_i (x : R) : normc (x*i) = normr x.
+Proof. by rewrite /normc/= expr0n //=  add0r sqrtr_sqr. Qed.
+
+Lemma normcN1 : normc (-1%:C) = 1 :> R.
+Proof. by rewrite /normc/=  oppr0 expr0n addr0 -signr_odd expr0 sqrtr1. Qed.
+
+Lemma realtocomplex_additive (x y : R) : (x + y)%:C = x%:C + y%:C.
+Proof.
+(*real_complex_additive*)
+rewrite -!complexr0 eqE_complex //=; by split; last by rewrite addr0.
+Qed.
+
+Lemma real_complex_inv (x : R) : x%:C^-1 = (x^-1)%:C.
+Proof. 
+(* Search _ (rmorphism _). *)
+have [/eqP->|x0] := boolP (x == 0); first by rewrite !invr0.
+apply/eqP; rewrite eq_complex /= mul0r oppr0 eqxx andbT expr0n addr0.
+by rewrite expr2 invrM ?unitfE // mulrA divrr ?unitfE // div1r.
+Qed.
+
+Lemma Im_inv : ('i%C)^-1 = (-1 *i) :> C.
+Proof. by rewrite complexiE invCi. Qed.
+
+Lemma invcM (x y : C) : (x * y)^-1 = x^-1 * y^-1.
+Proof.
+have [/eqP->|x0] := boolP (x == 0); first by rewrite !(invr0,mul0r).
+have [/eqP->|y0] := boolP (y == 0); first by rewrite !(invr0,mulr0).
+by rewrite invrM // mulrC.
+Qed.
+
+Lemma Im_mul (x : R) : x *i = x%:C * 'i%C.
+Proof. by simpc. Qed.
+
+Lemma normcD (x y : C) : normc (x + y) <= normc x + normc y.
+Proof. by rewrite -lecR realtocomplex_additive; apply: lec_normD. Qed.
+
+
+
+Lemma normc_ge0 (x : C) : 0 <= normc x.
+Proof. case: x => ? ?; exact: sqrtr_ge0. Qed.
+
+Lemma normc_gt0 (v : C) : (0 < normc v) = (v != 0).
+Proof.
+rewrite lt_neqAle normc_ge0 andbT; apply/idP/idP; apply/contra.
+by move/eqP ->; rewrite normc0.
+by rewrite eq_sym => /eqP/eq0_normc ->.
+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 real_complexM ( a b :R) : a%:C * b%:C = (a * b)%:C.
+Proof. by simpc. Qed.
+
+
+
+Lemma real_complexA (x : R) : x%:C%:A = x%:C :> C^o.
+Proof.
+by rewrite eqE_complex /=; split; rewrite ?mulr0 ?mul0r ?mulr1 ?addr0 ?subr0.
+Qed.
+
+
+Lemma lecM (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 normc_natmul (k : nat) : normc k%:R = k%:R :> R.
+Proof.
+by rewrite mulrnc /= mul0rn expr0n addr0 sqrtr_sqr ger0_norm // ler0n.
+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.
+move=> r0; have rr : r \is Num.real by rewrite realE (ltW r0).
+rewrite /normc (complexE r) /=; simpc.
+rewrite (ger0_Im (ltW r0)) expr0n addr0 sqrtr_sqr gtr0_norm ?complexr0 //.
+by move: r0; rewrite {1}(complexE r) /=; simpc => /andP[/eqP].
+Qed.
+
+Lemma gt0_real_complex (r : C) : 0 < r -> r = (Re r)%:C.
+Proof.
+by move=> r0; rewrite eqE_complex /=; split; last by apply: ger0_Im; apply: ltW.
+Qed.
+
+Lemma ltr0c  (k : R): (0 < k%:C) = (0 < k).
+Proof.  by simpc. Qed.
+
+
+Lemma complex_Re_gt0 (r : {posnum C}) :  0 < (complex.Re r%:num).
+Proof.  by rewrite -ltr0c -gt0_real_complex. Qed.
+
+
+Canonical complex_Re_posnum (x : {posnum C}) := PosNum (complex_Re_gt0 x).
+
+Lemma real_complex_gt0 (r : {posnum R}) :  0 < (r%:num)%:C.
+Proof. by rewrite ltcR. Qed.
+
+Canonical real_complex_posnum (x : {posnum R}) := PosNum (real_complex_gt0 x).
+
+
+Lemma real_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 complexV (*name ?*) (h: R) : h != 0 -> (h^-1)%:C = h%:C^-1.
+Proof.
+rewrite eqE_complex //=; split; last by rewrite mul0r oppr0.
+by rewrite expr0n //= addr0 -exprVn expr2 mulrA mulrV ?unitfE ?mul1r //=.
+Qed.
+
+(* Definition C_pointedType := PointedType C 0. *)
+(* Canonical C_pointedType. *)
+(* Definition C_filteredType := FilteredType C C (nbhs_ball_ (ball_ (@normc R)) ). *)
+(* Canonical C_filteredType. *)
+(* already in complexField*)
+End complex_extras.
+
+
+Section Holomorphe_der.
+Variable R : rcfType.
+
+Local Notation sqrtr := Num.sqrt.
+Local Notation C := R[i].
+Local Notation Re := (@complex.Re R).
+Local Notation Im := (@complex.Im R).
+
+
+
+Lemma is_cvg_scaler (K : numFieldType) (V : normedModType K) (T : topologicalType)
+ (F : set (set T)) (H :Filter F) (f : T -> V) (k : K) :
+ cvg (f @ F) -> cvg ((k \*: f) @ F ).
+Proof. by move => /cvg_ex [l H0] ; apply: cvgP; apply: cvgZr; apply: H0. Qed.
+
+Lemma limin_scaler (K : numFieldType) (V : normedModType K) (T : topologicalType)
+  (F : set (set T)) (FF : ProperFilter F) (f : T -> V) (k : K) :
+  cvg(f @ F) -> k *: lim (f @ F) = lim ((k \*: f) @ F ).
+Proof. by move => cv; apply/esym/cvg_lim => //; apply: cvgZr. Qed.
+
+Definition holomorphic (f : C -> C) (c : C) :=
+  cvg ((fun (h : C) => h^-1 *: ((f \o shift c) h - f c)) @ (nbhs' (0:C))).
+End Holomorphe_der.
+      
+
+
+Section holo_at.
+ Variable R : rcfType.
+
+Local Notation sqrtr := Num.sqrt.
+Local Notation C := R[i].
+Local Notation Re := (@complex.Re R).
+Local Notation Im := (@complex.Im R).
+
+ 
+  (*CR with the @ definitions *)
+  
+Definition real_complex : R^o -> C := ( fun r => r%:C ).
+(*make shorter *)
+
+Definition Rderivable_fromcomplex' (f : C -> C) (c v: C) :=
+  cvg ((fun (h : C) => h^-1 * ((f \o shift c) (h *:v) - f c)) @
+                                     (real_complex @ (nbhs' (0:R^o)))).
+
+Definition CauchyRiemanEq' (f : C -> C) z :=
+  'i * lim ( (fun h : C => h^-1 *: ((f \o shift z) (h) - f z)) @
+                                        (real_complex @ (nbhs' (0:R^o)))) =
+  lim ((fun h : C => h^-1 *: ((f \o shift z) (h * 'i) - f z)) @
+                                        (real_complex @ (nbhs' (0:R^o)))) .
+
+Lemma holo_derivable' (f : (C)^o -> (C)^o) c :
+  holomorphic f c -> (forall v : C, Rderivable_fromcomplex' f c v).
+Proof.
+move=> /cvg_ex; rewrite /type_of_filter /=.
+move => [l H]; rewrite /Rderivable_fromcomplex' => v /=.
+set quotR := (X in (X @ _)).
+simpl in (type of quotR).
+pose mulrv (h : R^o) := (h%:C * v).
+pose quotC (h : C^o) : C^o := h^-1 *: ((f \o shift c) h - f c).
+have -> :  quotR @ (real_complex @ nbhs' 0) =  (quotR \o (real_complex)) @ nbhs' 0 by []. 
+case: (v =P 0) =>  [eqv0|/eqP vneq0].
+  have -> :  quotR \o real_complex = 0.
+    apply: funext => h; rewrite  /quotR  /= eqv0.
+    by rewrite scaler0 add0r subrr mulr0 //=.
+  by apply: (cvgP (0:C^o)); apply: (cvg_cst (0 : C^o)).
+apply: (cvgP (v *: l)).
+have eqnear0: {near nbhs' 0, (v \*o quotC) \o mulrv =1 (quotR \o real_complex)}.
+(* as we need to perform computation for h != 0, we cannot prove fun equality directly *)
+  exists 1 => // h _ neq0h; rewrite /quotC /quotR /real_complex /mulrv //=.
+(*have -> :  (h *: v)^-1 = h^-1 *: v^-1. Fail rewrite (@invrZ R _ h _). *) (* issue with R^o*)
+  rewrite invrM ?unitfE //; last by rewrite neqCr0 ?unitfE.
+  by rewrite mulrA (mulrA v) mulrV ?unitfE // mul1r.
+have subsetfilters : quotR \o real_complex @ nbhs' 0 `=>` (v \*o quotC) \o mulrv @ nbhs' 0.
+by apply: (near_eq_cvg eqnear0).
+apply: cvg_trans subsetfilters _.
+suff: v \*o quotC \o mulrv @ nbhs' 0 `=>` nbhs (v *: l) by move/cvg_trans; apply.
+apply: (@cvg_comp _ _ _ _ _ _ (nbhs' (0:C^o))); last by apply: cvgZr.
+move => //= A [r leq0r /= ballrA].   exists ( normc r / normc v ).
+ by  rewrite mulr_gt0 // ?normc_gt0 ?gt_eqF //= ?invr_gt0 ?normc_gt0.
+move=> b ; rewrite /ball_ sub0r normrN => ballrb neqb0.
+have ballCrb : (@ball_ _ _ (fun x => `|x|) 0 r (mulrv b)).
+  rewrite /ball_ sub0r normrN /mulrv normrM.
+  rewrite ltr_pdivl_mulr in ballrb; last by rewrite normc_gt0.
+  by rewrite -(ger0_norm (ltW leq0r)) real_norm real_complexM ltcR.
+  by apply: (ballrA (mulrv b) ballCrb); apply mulf_neq0; rewrite ?eqCr.
+Qed.
+
+
+(*The fact that the topological structure is only available on C^o
+makes iterations of C^o apply *)
+
+(*The equality between 'i as imaginaryC from ssrnum and 'i is not transparent:
+ neq0ci is part of ssrnum and uneasy to find *)
+
+Lemma holo_CauchyRieman' (f : C -> C) c: holomorphic f c -> CauchyRiemanEq' f c.
+Proof. (* To be cleaned *)
+move=> /cvg_ex; rewrite /type_of_filter //= /CauchyRiemanEq'.
+set quotC := (fun h : R[i] => h^-1 *: (f (h + c) - f c)) . 
+simpl in (type of quotC).
+set quotR := fun h => h^-1 *: ((f \o shift c) (h * 'i) - f c) .
+simpl in (type of quotR).
+(* set locR0 := real_complex @ (nbhs' (0 : R^o)). *)
+move => [l H].
+have -> :  quotR @ (real_complex @ nbhs' 0) =  (quotR \o (real_complex)) @ nbhs' 0 by []. 
+have HR0:(quotC \o (real_complex) @ nbhs' 0)  --> l.
+  apply: cvg_comp; last by exact: H.
+  move => A [[r ri]];  rewrite ltcE=> /andP /= [/eqP -> r0]; rewrite complexr0 => ball.
+  exists r; first by [].
+  move=> a /=; rewrite sub0r normrN => ar aneq0.
+  apply: ball; last by rewrite eqCr.
+  by simpl; rewrite sub0r normrN ltcR normcr.
+have lem : quotC \o  *%R^~ 'i%R @ (real_complex @ (nbhs' (0 : R^o))) --> l.
+  apply: cvg_comp; last by exact: H.
+  move => A /= [ [r ri] ].
+  rewrite ltcE=> /andP /= [/eqP -> r0]; rewrite complexr0 => ball.
+  exists r; first by [].
+  move => a /= ; rewrite sub0r normrN => ar aneq0; apply: ball.
+    simpl; rewrite sub0r normrN normrM /=.
+    have ->: `|'i| = 1 by move => T;  simpc; rewrite expr0n expr1n /= add0r sqrtr1.
+    by rewrite mulr1 ltcR normcr.
+  apply: mulf_neq0; last by rewrite neq0Ci.
+  by rewrite eqCr.
+have HRcomp:  cvg (quotC \o *%R^~ 'i%R @ (real_complex @ (nbhs' (0 : R^o)))) .
+  by apply/cvg_ex;  simpl; exists l.
+have ->: lim (quotR @ (real_complex @ (nbhs' (0 : R^o))))
+  = 'i *: lim (quotC \o ( fun h => h *'i) @ (real_complex @ (nbhs' (0 : R^o)))).
+  have: 'i \*:quotC \o ( fun h => h *'i) =1 quotR.
+  move => h /= ;rewrite /quotC /quotR /=.
+  rewrite invcM scalerA mulrC -mulrA mulVf.
+    by rewrite mulr1.
+    by rewrite neq0Ci.
+by move => /funext <-; rewrite (limin_scaler _ 'i HRcomp).
+rewrite scalecM.
+suff: lim (quotC @ (real_complex @ (nbhs' (0 : R^o))))
+      = lim (quotC \o  *%R^~ 'i%R @ (real_complex @ (nbhs' (0 : R^o)))) by move => -> .
+suff -> : lim (quotC @ (real_complex @ (nbhs' (0 : R^o)))) = l.
+  apply/eqP; rewrite eq_sym; apply/eqP. apply: (cvg_map_lim _ lem).
+  by apply: norm_hausdorff. 
+by apply: (@cvg_map_lim ((numFieldType_regular_topologicalType (complex_numFieldType R))));
+first by apply: norm_hausdorff.
+Qed.
+
+End holo_at.
+
+Module CR_holo.
+Variable (R: realType). (* new, because of proper_filter_nbhs'*)
+Notation C := R[i].
+
+Definition Rcomplex := R[i].
+Canonical Rcomplex_eqType := [eqType of Rcomplex].
+Canonical Rcomplex_choiceType := [choiceType of Rcomplex].
+Canonical Rcomplex_zmodType := [zmodType of Rcomplex].
+
+Canonical Rcomplex_lmodType := LmodType R Rcomplex (complex_lmodMixin R). 
+
+Canonical Rcomplex_ringType := [ringType of Rcomplex]. 
+
+Canonical Rcomplex_pointedType := [pointedType of Rcomplex].
+
+Canonical Rcomplex_filteredType :=
+  FilteredType Rcomplex Rcomplex (nbhs_ball_ (ball_ (@normc R))). 
+
+Definition Rcomplex_normedZmodMixin :=
+  @Num.NormedMixin R (Rcomplex_zmodType) _ _ (@normcD R)
+                   (@eq0_normc R) (@normc_mulrn R) (@normcN R).
+
+
+Canonical Rcomplex_normedZmodType :=
+  NormedZmodType R (Rcomplex) Rcomplex_normedZmodMixin.
+
+Definition Rcomplex_pseudoMetricMixin :=
+  (@pseudoMetric_of_normedDomain R (Rcomplex_normedZmodType)).
+
+Definition Rcomplex_topologicalMixin :=
+  (* topologyOfEntourageMixin (uniformityOfBallMixin *)
+  (*     (@nbhs_ball_normE R (Rcomplex_normedZmodType) ) *)
+  (*     Rcomplex_pseudoMetricMixin). *)
+  (topologyOfEntourageMixin  (uniformityOfBallMixin
+      (@nbhs_ball_normE R [normedZmodType R of Rcomplex])
+      (pseudoMetric_of_normedDomain [normedZmodType R of Rcomplex]))).
+
+
+Canonical Rcomplex_topologicalType :=
+  TopologicalType Rcomplex Rcomplex_topologicalMixin.
+
+
+
+Lemma Rcomplex_nbhsE : nbhs_ball_ (ball_ (@normc R)) =
+                       nbhs_ (entourage_ (ball_ (@normc R))).
+Proof.
+rewrite predeq2E => x A /=; split; rewrite /entourage_ /nbhs_ball_ /filter_from /=.
+Admitted.
+
+
+Definition Rcomplex_uniformMixin :=
+  uniformityOfBallMixin  (@nbhs_ball_normE R [normedZmodType R of Rcomplex])  (* Rcomplex_nbhsE *)
+                         Rcomplex_pseudoMetricMixin.
+
+Canonical Rcomplex_uniformType := UniformType Rcomplex Rcomplex_uniformMixin.
+
+Canonical Rcomplex_pseudoMetricType :=
+  PseudoMetricType Rcomplex_normedZmodType Rcomplex_pseudoMetricMixin.
+
+
+Lemma Rcomplex_ball_ball_ :
+  @ball _ (Rcomplex_pseudoMetricType ) = ball_ (fun x => `| x |).
+Proof. by []. Qed.
+
+Definition Rcomplex_pseudoMetricNormedZmodMixin :=
+  PseudoMetricNormedZmodule.Mixin Rcomplex_ball_ball_.
+
+Canonical Rcomplex_pseudoMetricNormedZmodType :=
+  PseudoMetricNormedZmodType R (Rcomplex_normedZmodType)
+                       Rcomplex_pseudoMetricNormedZmodMixin.
+
+Lemma normcZ  : forall (l : R), forall (x : Rcomplex), normc (l *: x) = `|l| * (normc x).
+Proof.
+by move => l; case=> ? ?; rewrite /normc //= !exprMn -mulrDr sqrtrM ?sqr_ge0 // sqrtr_sqr.
+Qed.
+
+
+Definition Rcomplex_normedModMixin :=
+  @NormedModMixin R (Rcomplex_pseudoMetricNormedZmodType)  _ (normcZ).
+
+Canonical Rcomplex_normedModType :=
+  NormedModType R _ Rcomplex_normedModMixin.
+
+(* Lemma scale_inv (h : R) (v : Rcomplex_lmodType) : h != 0 -> v != 0 -> (h *: v)^-1 = h^-1 *: v^-1. (* scaleCV *) *)
+(* Proof. *)
+(* by move=> h0 v0; rewrite scalecr invrM // ?unitfE ?eqCr // mulrC scalecr real_complex_inv. *)
+(* Qed. *)
+
+
+Lemma real_complexZ (a : R) (b : Rcomplex) : a%:C * b = a *: b.
+Proof. rewrite eqE_complex //=; split. 
+Admitted.
+
+
+Lemma scalecr : forall w : Rcomplex, forall r : R, (r *: w = r%:C *: w).
+Proof. by move=> [a b] r; rewrite eqE_complex //=; split; simpc. Qed.
+
+Lemma real_complex_alg (a : R) :  a *: (1 :Rcomplex)   = (@real_complex R) a.
+Proof.
+by apply/eqP; rewrite eq_complex; apply/andP; split; simpl; apply/eqP; rewrite ?mulr1 ?mulr0. 
+Qed. Search "real" in complex.
+
+
+Lemma scalecAl (h : R) (x y : Rcomplex): h *: (x * y) = h *: x * y.
+Proof.
+by move: h x y => h [a b] [c d]; simpc; rewrite -!mulrA -mulrBr -mulrDr.
+Qed.
+
+Definition C_RLalg := LalgType R (Rcomplex) scalecAl.
+
+(* Definition locR0 := (within (@Real_line R) (nbhs' 0)). *)
+
+Lemma complex0 : 0%:C = 0 :> C.
+Proof. rewrite eqE_complex //=. Qed.
+
+(* Should Real_Line be a proper subtype of C *)
+(* TBA: type of hausdorff topologicaltype *)
+
+Lemma cvg_compE ( T U V : topologicalType)
+      (f : T -> U) (g : V -> T)
+      (F : set ( set V)) :
+  cvg (f @ (g @ F)) <-> cvg (f \o g @ F).
+Proof.
+  by [].
+Qed.
+
+Lemma lim_compE ( T U V : topologicalType)
+      (f : T -> U) (g : V -> T)
+      (F : set ( set V)) :
+  lim (f @ (g @ F)) = lim (f \o g @ F).
+Proof.
+  by [].
+Qed.
+
+
+
+(*** Tentative proof with the @ notations ***)
+
+(*As norms on Rcomplex and C^o are equal, we are able to prove the following *)
+(*would be great to generalize to equivalent norms *)
+
+(* Notation "F --> l in T" := (@cvg_to T [filter of F] [filter of l]) (at level 70). *)
+
+
+Lemma complex_limP (F : set (set C))  (l : C):
+  (F --> (l: C^o)) <-> ( F --> (l :Rcomplex)).
+(* @cvg_to C^o F [filter of l] <-> @cvg_to Rcomplex F [filter of l].   *)
+(* Notation "F --> l in T" := (@cvg_to T [filter of F] [filter of l]) (at level 70). is too strong *)
+Proof.
+split; move => /= H A /=. 
+  move/(nbhs_ex (x:=l : Rcomplex_normedModType)) =>  [[r r0] /=].
+  rewrite -ball_normE /= => Br.
+  have : nbhs (l: C^o) A.
+    exists r%:C; first by rewrite ltcR.
+    by move => y /=; rewrite ltcR; apply: Br.
+  by move/(H A).
+move/(nbhs_ex (x:=l : C^o))=>  [[[r ri] r0] /=].
+move: r0; rewrite ltcE /= => /andP [/eqP ri0 r0] //.
+rewrite -ball_normE ri0 complexr0 /= => Br.
+have : nbhs (l: Rcomplex) A.
+  by exists r; last by move => y /=; rewrite -ltcR; apply: Br.
+by move/(H A).
+Qed.
+
+Check numFieldType_filteredType.
+
+Lemma complex_cvgP (F : set (set C)) (FF: Filter F) : [cvg F in Rcomplex_normedModType] <->
+   [cvg F in ((numFieldType_filteredType  (complex_numFieldType R)))].
+Proof.
+split; move/cvg_ex => /= [l H].
+  apply: (cvgP (l : (numFieldType_filteredType (complex_numFieldType R)))).
+  by apply/complex_limP.
+by apply: (cvgP (l : Rcomplex_filteredType )); apply/complex_limP.
+Qed.
+
+
+Lemma complex_liminP (F : set (set C)) (FF: ProperFilter F):
+   [lim F in Rcomplex_normedModType] =
+   [lim F in ((numFieldType_filteredType  (complex_numFieldType R)))].
+Proof.
+case: (EM ([cvg F in ((numFieldType_filteredType  (complex_numFieldType R)))])).
+  move/cvg_ex=> /= [l Fl].
+  rewrite (@norm_cvg_lim _ (numFieldType_normedModType _)   _ _ l) //.
+  by apply: (@norm_cvg_lim _ (Rcomplex_normedModType)); apply/complex_limP.
+move => dvg; pose copy := dvg ;move/dvgP: copy => ->.
+by move/complex_cvgP/dvgP: dvg => ->.
+Qed.
+
+(* here notations are misleading and don't show the different topologies
+at the target *)
+
+Notation  "f %:Rfun" :=
+  (f : (Rcomplex_normedModType) -> (Rcomplex_normedModType))
+  (at level 10, left associativity, format "f %:Rfun")  : complex_scope.
+
+Notation  "v %:Rcomplex" :=
+  (v : Rcomplex)
+    (at level 10, left associativity, format "v %:Rcomplex")  : complex_scope.
+
+Lemma Rdiff' (f : C -> C) c v:
+  (Rderivable_fromcomplex' f c v) <->
+  (derivable (f%:Rfun) c v).
+Proof.
+rewrite /Rderivable_fromcomplex' /derivable cvg_compE.
+have -> :  (fun h : (R[i]) => h^-1 * ((f \o shift c) (h *: v) - f c)) \o
+  real_complex (R:=R)  =   (fun h : R => h^-1 *: ((f \o shift c) (h *: v%:Rcomplex) - f c)).
+  by apply: funext => h /=; rewrite real_complex_inv -scalecM -!scalecr.
+by split;  move/complex_cvgP => /=.
+Qed.
+
+
+
+Lemma Rdiff1 (f : C^o -> C^o) c:
+          lim ( (fun h : C^o => h^-1 *: ((f \o shift c) (h) - f c))
+                 @ (((@real_complex R))@ (nbhs' (0:R^o))))
+         = 'D_1 (f%:Rfun) c.
+Proof.
+rewrite /derive lim_compE.
+suff -> :  (fun h : (R[i])^o => h^-1 * ((f \o shift c) (h ) - f c)) \o
+real_complex (R:=R) = fun h : R => h^-1 *: ((f \o shift c) (h *: (1 : C^o)) - f c).
+  by rewrite complex_liminP /=.
+apply: funext => h /=.
+by rewrite real_complex_inv -scalecM -!scalecr real_complex_alg.
+Qed.
+
+
+Lemma Rdiffi (f : C^o -> C^o) c:
+         lim ( (fun h : C^o => h^-1 *: ((f \o shift c) (h * 'i) - f c))
+                 @ (((@real_complex R))@ (nbhs' (0:R^o))))
+         = 'D_('i) (f%:Rfun) c. 
+Proof.
+rewrite /derive lim_compE.
+suff -> :  (fun h : (R[i])^o => h^-1 * ((f \o shift c) (h * 'i) - f c)) \o
+real_complex (R:=R) = fun h : R => h^-1 *: ((f \o shift c) (h *: ('i : Rcomplex)) - f c).
+  by rewrite complex_liminP /=.
+apply: funext => h /=.
+by rewrite real_complex_inv -scalecM -!scalecr real_complexZ.
+Qed.
+
+Lemma continuous_near (T U: topologicalType) (f: T -> U) (P : set U) (a : T):
+ (f @ a --> f a) -> ((\forall x \near nbhs (f a), P x)
+                           -> (\forall y \near nbhs a, P (f y))).
+Proof. by move/(_ P) => /=; near_simpl. Qed.
+
+
+Lemma holomorphicP (f : C^o -> C^o)  c : holomorphic f c <-> derivable f c 1.
+Proof.
+rewrite /holomorphic /derivable.
+have lem : forall (h : C^o), h%:A = h.
+by move => h; rewrite [h *: 1]/(h *1) //=; apply: mulr1. (*Fail, rewrite mulr1 does not work *)
+suff -> : (fun h => h^-1 *: ((f \o shift c) h - f c)) =
+             ((fun h  => h^-1 *: ((f \o shift c) h%:A - f c))) by []. (* time *)
+by apply: funext => h;  rewrite lem.
+Qed.
+
+
+
+(* Variable (f : C^o -> C^o). Fail Check (differentiable f)  ???*)
+
+Lemma real_normc_ler (x y : R) :
+  `|x| <= normc (x +i* y).
+Proof.
+rewrite /normc /= -ler_sqr ?nnegrE ?normr_ge0 ?sqrtr_ge0 //.
+rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=; last by apply: num_real.
+by rewrite ler_addl ?sqr_ge0.
+Qed.
+
+Lemma im_normc_ler (x y : R) :
+  `|y| <= normc (x +i* y).
+Proof.
+rewrite /normc /= -ler_sqr ?nnegrE ?normr_ge0 ?sqrtr_ge0 //.
+rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=; last by apply: num_real.
+by rewrite ler_addr ?sqr_ge0.
+Qed.
+
+Lemma num_posnum  (K : numDomainType) (x : K) (x0 : 0 < x) :
+  (PosNum x0)%:num = x.
+Proof. by []. Qed.
+
+Lemma eq_deriv_real_complex (f : C^o -> C^o)  c:
+  (forall v : C^o, Rderivable_fromcomplex' f c v) ->
+  ('D_1 f c = 'D_1 (f%:Rfun) c)/\ ('D_'i f c = 'D_'i  (f%:Rfun) c).
+Proof. (* part of holo -> Rder *) Admitted.   
+
+Lemma Diff_CR_holo' (f : C^o -> C^o)  c:
+  (forall v : C^o, Rderivable_fromcomplex' f c v) /\ {for c, continuous ('D_'i f)} /\
+  {for c, continuous ('D_1 f)}
+  (* (differentiable f%:Rfun c) *)
+  /\ (CauchyRiemanEq' f c)
+  -> (holomorphic f c).
+Proof.
+move=> [der [Dic [D1c CR]]]; apply/holomorphicP; apply/derivable_nbhsP /eqaddoP => eps eps0 /=.
+rewrite (gt0_real_complex eps0) /=. 
+set e := complex.Re eps.
+pose e5 := (e/5%:R)%:C.
+have e50 : 0< e5 by admit.
+(* Beware that *:%R^~ ('D_1 f c)))  is in C^o *)
+(* move /(_ c (ball_ (normr) (('D_'i%C f c)) (e5))  (nbhsx_ballx (('D_'i%C f c)) *)
+(*      ((PosNum e50)))): Dic;  simpl. *)
+(* move /nbhs_ex => //=  [[[di dii]]] /=; rewrite ltcE /= => /andP [/eqP ->  di0] /=. *)
+(* rewrite complexr0=> Dic. *)
+(* move /(_ c (ball_ (normr) (('D_1 f c)) (e5))  (nbhsx_ballx (('D_1 f c)) *)
+(*       ((PosNum e50)))): D1c;  simpl. *)
+(* move /nbhs_ex => //=  [[[d1 d1i]]] /=; rewrite ltcE /= => /andP [/eqP -> d10] /=. *)
+(* rewrite complexr0=> D1c; rewrite nearE /=. *)
+rewrite nearE /=.
+move/Rdiff': (der (1 : C^o)); move/derivable_nbhsP/eqaddoP/(_ (e/5%:R)).
+elim; last by  rewrite ?mulr_gt0 //= /e -ltr0c -(gt0_real_complex eps0).
+move => r1 r10;  rewrite /ball_ //= => h1.
+move/Rdiff': (der ('i : C^o)); move/derivable_nbhsP/eqaddoP/(_ (e/5%:R)).
+elim; last by rewrite ?mulr_gt0 //= /e -ltr0c -(gt0_real_complex eps0).
+move => ri  ri0; rewrite /ball_ //= => hi.
+move /(_  (ball_ (normr) (('D_'i%C f c)) (e5))  (nbhsx_ballx (('D_'i%C f c))
+     ((PosNum e50)))): Dic;  simpl.
+move /nbhs_ex => //=  [[[di dii]]] /=; rewrite ltcE /= => /andP [/eqP ->  di0] /=.
+rewrite complexr0=> Dic.
+move /(_  (ball_ (normr) (('D_1 f c)) (e5))  (nbhsx_ballx (('D_1 f c))
+      ((PosNum e50)))): D1c;  simpl.
+move /nbhs_ex => //=  [[[d1 d1i]]] /=; rewrite ltcE /= => /andP [/eqP -> d10] /=.
+rewrite complexr0=> D1c.
+pose r :=  minr di (minr (minr ri r1)  d1).
+exists r%:C.
+  rewrite ltr0c /r.
+  rewrite -(num_posnum d10) -(num_posnum ri0) -(num_posnum r10) -(num_posnum di0).
+  by apply: min_pos_gt0.
+move => [x y] /=; rewrite sub0r normrN //= => hri //=.
+set fh := (X in `|X| <= _); simpl in (type of fh).
+have->: fh =  (f((x +i* y)*:1 + c) - (f c +  (x +i* y)*:('D_1 f c))) by [].
+have x1 : `|x| < r1.
+apply: le_lt_trans; first by apply: real_normc_ler.
+apply: lt_le_trans; first  by rewrite -ltcR; exact: hri.
+by rewrite /r !le_minl; apply/orP; right; apply/orP; left; apply/orP; right.
+have yi : `|y| < ri.
+apply: le_lt_trans; first by apply: (im_normc_ler x).
+apply: lt_le_trans; first by rewrite -ltcR; exact: hri.
+by rewrite /r !le_minl; apply/orP;  right; apply/orP; left; apply/orP; left.
+move: (hi y) ; simpl; rewrite sub0r normrN; move /(_ yi) {hi}.
+set a := (fun h : R => f (h *: 'i%C + c)).
+set b := ((cst (f c)) : R -> C^o).
+set diff := (X in  (b + X)). (*necessary*)
+have ->: (a - (b + diff))y = a y - (b y + diff y) by [].
+rewrite /a/b/diff /=  => hi.
+move: (h1 x); simpl; rewrite sub0r normrN; move /(_ x1) {h1 a b diff}.
+set a := (fun h : R => f (h*:(1 : C^o) + c)).
+set b := ((cst (f c)) : R -> C^o).
+set diff :=  (X in (b + X)). (* necessary *)
+have -> : (a - (b + diff)) x = a x - ( b x + diff x) by [].
+rewrite /a/b/diff.
+move => h1 {a b diff}.
+rewrite !scalecM.
+have -> : (x +i* y) * 'D_1 f c = x *: 'D_1 f%:Rfun c  + y *: 'D_('i) f%:Rfun c.
+  have -> :  (x +i* y) = ( x%:C *: 1 + (y%:C) *: ('i : C^o)) by simpc.
+  move : CR; rewrite /CauchyRiemanEq' Rdiff1 Rdiffi.
+  move : (eq_deriv_real_complex der) => [ ->  -> ] <-.
+  rewrite -!real_complexZ mulrA //.
+  by rewrite -mulrDl //= real_complexA scalecM.
+have -> :
+  f ((x +i* y)%:A + c) - (f c + (x *: 'D_1 f c + y *: 'D_'i f c)) =
+    (f (x%:C + c + y*:('i%C) ) - (f (c + y*:('i%C)) +  x *: 'D_1 f (c + y*:'i%C)) +
+    (f (y *: 'i%C + c) - (f c + y *: 'D_'i%C f (c))) +
+    ( x *: 'D_1 f (c + y*:'i%C) -  x *: 'D_1 f (c))). admit.
+apply: le_trans; first by apply: ler_norm_add.
+apply: le_trans; first by apply: ler_add; first by apply:ler_norm_add.
+
+Admitted.
diff --git a/theories/normedtype.v b/theories/normedtype.v
index c5d99b96c6..a34e1ec92f 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -1,8 +1,9 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice.
 From mathcomp Require Import seq fintype bigop order ssralg ssrint ssrnum finmap.
-From mathcomp Require Import matrix interval zmodp.
+From mathcomp Require Import matrix interval zmodp vector fieldext falgebra.
 Require Import boolp ereal reals.
+
 Require Import classical_sets posnum topology prodnormedzmodule.
 
 (******************************************************************************)
@@ -268,25 +269,301 @@ by move=> [E [e egt0 sbeE] sEA]; exists e => // ??; apply/sEA/sbeE.
 Qed.
 End pseudoMetric_of_normedDomain.
 
-Section numFieldType_canonical.
+Section vecspace_of_numfield. (*NEW*)
+  (*TODO: put all results on ^o in a separate module (C. Cohen suggestion) *)
+  (* !! Redundant with ^o *)
+  (* While there may not be a canonical algebra on each ring, we assume here  *)
+  (* there is a canonical vecspace on each field. We make use of the          *)
+  (* canonical algebraic structures defined on regular algebras in mathcomp   *)
+  
+Canonical numField_lmodType (K : numFieldType) :=
+  [lmodType K of K for [lmodType K of K^o]].
+Canonical numField_lalgType (K : numFieldType) :=
+  [lalgType K of K for [lalgType K of K^o]].
+Canonical numField_algType (K : numFieldType) :=
+  [algType K of K for [algType K of K^o]].
+Canonical numField_comAlgType (K : numFieldType) :=   [comAlgType K of K].
+Canonical numField_unitAlgType (K : numFieldType) := [unitAlgType K of K].
+Canonical numField_comUnitAlgType (K : numFieldType) := [comUnitAlgType K of K].
+Canonical numField_vectType (K : numFieldType) :=
+  [vectType K of K for [vectType K of K^o]].
+Canonical numField_falgType (K : numFieldType) := [FalgType K of K].
+Canonical numField_fieldExtType (K : numFieldType) :=
+  [fieldExtType K of K for regular_fieldExtType K].
+
+Canonical numClosedField_lmodType (K : numClosedFieldType) :=
+  [lmodType K of K for [lmodType K of K^o]].
+Canonical numClosedField_lalgType (K : numClosedFieldType) :=
+  [lalgType K of K for [lalgType K of K^o]].
+Canonical numClosedField_algType (K : numClosedFieldType) :=
+  [algType K of K for [algType K of K^o]].
+Canonical numClosedField_comAlgType (K : numClosedFieldType) :=
+  [comAlgType K of K].
+Canonical numClosedField_unitAlgType (K : numClosedFieldType) :=
+  [unitAlgType K of K].
+Canonical numClosedField_comUnitAlgType (K : numClosedFieldType) :=
+  [comUnitAlgType K of K].
+Canonical numClosedField_vectType (K : numClosedFieldType) :=
+  [vectType K of K for [vectType K of K^o]].
+Canonical numClosedField_falgType (K : numClosedFieldType) := [FalgType K of K].
+Canonical numClosedField_fieldExtType (K : numClosedFieldType) :=
+  [fieldExtType K of K for regular_fieldExtType K].
+
+Canonical realField_lmodType (K : realFieldType) :=
+  [lmodType K of K for [lmodType K of K^o]].
+Canonical realField_lalgType (K : realFieldType) :=
+  [lalgType K of K for [lalgType K of K^o]].
+Canonical realField_algType (K : realFieldType) :=
+  [algType K of K for [algType K of K^o]].
+Canonical realField_comAlgType (K : realFieldType) := [comAlgType K of K].
+Canonical realField_unitAlgType (K : realFieldType) := [unitAlgType K of K].
+Canonical realField_comUnitAlgType (K : realFieldType) :=
+  [comUnitAlgType K of K].
+Canonical realField_vectType (K : realFieldType) :=
+  [vectType K of K for [vectType K of K^o]].
+Canonical realField_falgType (K : realFieldType) := [FalgType K of K].
+Canonical realField_fieldExtType (K : realFieldType) :=
+  [fieldExtType K of K for regular_fieldExtType K].
+
+Canonical archiField_lmodType (K : archiFieldType) :=
+  [lmodType K of K for [lmodType K of K^o]].
+Canonical archiField_lalgType (K : archiFieldType) :=
+  [lalgType K of K for [lalgType K of K^o]].
+Canonical archiField_algType (K : archiFieldType) :=
+  [algType K of K for [algType K of K^o]].
+Canonical archiField_comAlgType (K : archiFieldType) := [comAlgType K of K].
+Canonical archiField_unitAlgType (K : archiFieldType) := [unitAlgType K of K].
+Canonical archiField_comUnitAlgType (K : archiFieldType) :=
+  [comUnitAlgType K of K].
+Canonical archiField_vectType (K : archiFieldType) :=
+  [vectType K of K for [vectType K of K^o]].
+Canonical archiField_falgType (K : archiFieldType) := [FalgType K of K].
+Canonical archiField_fieldExtType (K : archiFieldType) :=
+  [fieldExtType K of K for regular_fieldExtType K].
+
+Canonical rcf_lmodType (K : rcfType) :=
+  [lmodType K of K for [lmodType K of K^o]].
+Canonical rcf_lalgType (K : rcfType) :=
+  [lalgType K of K for [lalgType K of K^o]].
+Canonical rcf_algType (K : rcfType) := [algType K of K for [algType K of K^o]].
+Canonical rcf_comAlgType (K : rcfType) := [comAlgType K of K].
+Canonical rcf_unitAlgType (K : rcfType) := [unitAlgType K of K] .
+Canonical rcf_comUnitAlgType (K : rcfType) := [comUnitAlgType K of K].
+Canonical rcf_vectType (K : rcfType) :=
+  [vectType K of K for [vectType K of K^o]].
+Canonical rcf_falgType (K : rcfType) := [FalgType K of K].
+Canonical rcf_fieldExtType (K : rcfType) :=
+  [fieldExtType K of K for regular_fieldExtType K].
+
+Canonical real_lmodType (K : realType) :=
+  [lmodType K of K for [lmodType K of K^o]].
+Canonical real_lalgType (K : realType) :=
+  [lalgType K of K for [lalgType K of K^o]].
+Canonical real_algType (K : realType) :=
+  [algType K of K for [algType K of K^o]].
+Canonical real_comAlgType (K : realType) := [comAlgType K of K].
+Canonical real_unitAlgType (K : realType) := [unitAlgType K of K].
+Canonical real_comUnitAlgType (K : realType) := [comUnitAlgType K of K].
+Canonical real_vectType (K : realType) :=
+  [vectType K of K for [vectType K of K^o]].
+Canonical real_falgType (K : realType) := [FalgType K of K].
+Canonical real_fieldExtType (K : realType) :=
+  [fieldExtType K of K for regular_fieldExtType K].
+
+
+Coercion numField_lmodType : numFieldType >-> lmodType.
+Coercion numField_lalgType : numFieldType >-> lalgType.
+Coercion numField_comAlgType : numFieldType >-> comAlgType. (* ambiguous path *)
+Coercion numField_unitAlgType : numFieldType >-> unitAlgType.
+Coercion numField_comUnitAlgType : numFieldType >-> comUnitAlgType. (* ambiguous path *)
+Coercion numField_vectType  : numFieldType >-> vectType.
+Coercion numField_falgType : numFieldType >-> FalgType.
+Coercion numField_fieldExtType : numFieldType >-> fieldExtType. (* ambiguous path *)
+
+
+
+(* TODO : other coercions *)
+
+End vecspace_of_numfield.
+
+
+
+Section numField_topological. (*New *)
+Variable  (R: numFieldType).
+Canonical numFieldType_pointedType (R: numFieldType) :=
+  [pointedType of R for pointed_of_zmodule R].
+Canonical numFieldType_filteredType (R: numFieldType) :=
+  [filteredType R of R for filtered_of_normedZmod R].
+Canonical numFieldType_topologicalType (R: numFieldType) : topologicalType := TopologicalType R
+  (topologyOfEntourageMixin
+    (uniformityOfBallMixin
+      (@nbhs_ball_normE _ [normedZmodType R of R])
+      (pseudoMetric_of_normedDomain [normedZmodType R of R]))).
+Canonical numFieldType_uniformType (R: numFieldType) : uniformType := UniformType R
+  (uniformityOfBallMixin (@nbhs_ball_normE _ [normedZmodType R of R])
+    (pseudoMetric_of_normedDomain [normedZmodType R of R])).
+Canonical numFieldType_pseudoMetricType (R: numFieldType)
+  := @PseudoMetric.Pack R R (@PseudoMetric.Class R R
+     (Uniform.class (numFieldType_uniformType R)) (@pseudoMetric_of_normedDomain R R)).
+
+
+Canonical numClosedFieldType_pointedType (R: numClosedFieldType) :=
+  [pointedType of R for [pointedType of [numFieldType of R]]].
+Canonical numClosedFieldType_filteredType (R: numClosedFieldType) :=
+  [filteredType _ of R for [filteredType _ of [numFieldType of R]]].
+Canonical numClosedFieldType_topologicalType (R: numClosedFieldType) : topologicalType :=
+  (* [topologicalType of R for [topologicalType of [numFieldType of R]]]. *)
+  (*leads to ambiguous path *)
+  TopologicalType R
+  (topologyOfEntourageMixin
+    (uniformityOfBallMixin
+      (@nbhs_ball_normE _ [normedZmodType R of R])
+      (pseudoMetric_of_normedDomain [normedZmodType R of R]))).
+Canonical numClosedFieldType_pseudoMetricType (R: numClosedFieldType) :=
+ (* [pseudoMetricType _ of R for [pseudoMetricType _ of [numFieldType of R]]]. *)
+ (* leads to ambiguous path *)
+  @PseudoMetric.Pack R R (@PseudoMetric.Class R R
+     (Uniform.class (numFieldType_uniformType R)) (@pseudoMetric_of_normedDomain R R)).
+
+Canonical realFieldType_pointedType (R: realFieldType) :=
+  [pointedType of R for [pointedType of [numFieldType of R]]].
+Canonical realFieldType_filteredType (R: realFieldType) :=
+ [filteredType _ of R for [filteredType _ of [numFieldType of R]]].
+Canonical realFieldType_topologicalType (R: realFieldType) : topologicalType :=
+  (* [topologicalType of R for [topologicalType of [numFieldType of R]]]. *)
+  (*leads to ambiguous path *)
+  TopologicalType R
+  (topologyOfEntourageMixin
+    (uniformityOfBallMixin
+      (@nbhs_ball_normE _ [normedZmodType R of R])
+      (pseudoMetric_of_normedDomain [normedZmodType R of R]))). 
+Canonical realFieldType_pseudoMetricType (R: realFieldType) :=
+ (* [pseudoMetricType _ of R for [pseudoMetricType _ of [numFieldType of R]]]. *)
+ (* leads to ambiguous path *)
+   @PseudoMetric.Pack R R (@PseudoMetric.Class R R
+     (Uniform.class (numFieldType_uniformType R)) (@pseudoMetric_of_normedDomain R R)). 
+
+Canonical archiFieldType_pointedType (R: archiFieldType) :=
+  [pointedType of R for [pointedType of [numFieldType of R]]].
+Canonical archiFieldType_filteredType (R: archiFieldType) :=
+  [filteredType _ of R for [filteredType _ of [numFieldType of R]]].
+Canonical archiFieldType_topologicalType (R: archiFieldType) : topologicalType :=
+ (* [topologicalType of R for [topologicalType of [numFieldType of R]]]. *)
+  (*leads to ambiguous path *)
+ TopologicalType R
+  (topologyOfEntourageMixin
+    (uniformityOfBallMixin
+      (@nbhs_ball_normE _ [normedZmodType R of R])
+      (pseudoMetric_of_normedDomain [normedZmodType R of R]))).
+Canonical archiFieldType_pseudoMetricType (R: archiFieldType):=
+   (* [pseudoMetricType _ of R for [pseudoMetricType _ of [numFieldType of R]]]. *)
+ (* leads to ambiguous path *)
+  @PseudoMetric.Pack R R (@PseudoMetric.Class R R
+     (Uniform.class (numFieldType_uniformType R)) (@pseudoMetric_of_normedDomain R R)).
+
+Canonical rcfType_pointedType (R: rcfType) :=
+  [pointedType of R for [pointedType of [numFieldType of R]]].
+Canonical rcfType_filteredType (R: rcfType) :=
+  [filteredType R of R for filtered_of_normedZmod R].
+Canonical rcfType_topologicalType (R: rcfType) : topologicalType :=
+ (* [topologicalType of R for [topologicalType of [numFieldType of R]]]. *)
+  (*leads to ambiguous path *)
+TopologicalType R
+  (topologyOfEntourageMixin
+    (uniformityOfBallMixin
+      (@nbhs_ball_normE _ [normedZmodType R of R])
+      (pseudoMetric_of_normedDomain [normedZmodType R of R]))).
+Canonical rcfType_pseudoMetricType (R: rcfType) :=
+  (* [pseudoMetricType _ of R for [pseudoMetricType _ of [numFieldType of R]]]. *)
+ (* leads to ambiguous path *)
+ @PseudoMetric.Pack R R (@PseudoMetric.Class R R
+     (Uniform.class (numFieldType_uniformType R)) (@pseudoMetric_of_normedDomain R R)).
+
+Canonical realType_pointedType (R: realType) :=
+  [pointedType of R for [pointedType of [numFieldType of R]]].
+Canonical realType_filteredType (R: realType) :=
+  [filteredType _ of R for [filteredType _ of [numFieldType of R]]].
+Canonical realType_topologicalType (R: realType) : topologicalType :=
+ (* [topologicalType of R for [topologicalType of [numFieldType of R]]]. *)
+  (*leads to ambiguous path *)
+ TopologicalType R
+  (topologyOfEntourageMixin
+    (uniformityOfBallMixin
+      (@nbhs_ball_normE _ [normedZmodType R of R])
+      (pseudoMetric_of_normedDomain [normedZmodType R of R]))).
+Canonical realType_pseudoMetricType (R: realType) :=
+  (* [pseudoMetricType _ of R for [pseudoMetricType _ of [numFieldType of R]]]. *)
+ (* leads to ambiguous path *)
+@PseudoMetric.Pack R R (@PseudoMetric.Class R R
+     (Uniform.class (numFieldType_uniformType R)) (@pseudoMetric_of_normedDomain R R)).
+
+Coercion numFieldType_pointedType : numFieldType >-> pointedType.
+Coercion numFieldType_filteredType : numFieldType >-> filteredType.
+Coercion numFieldType_topologicalType : numFieldType >-> topologicalType.
+Coercion numFieldType_pseudoMetricType : numFieldType >-> pseudoMetricType.
+
+Coercion numClosedFieldType_pointedType : numClosedFieldType >-> pointedType.
+Coercion numClosedFieldType_filteredType : numClosedFieldType >-> filteredType.
+Coercion numClosedFieldType_topologicalType : numClosedFieldType >-> topologicalType.
+Coercion numClosedFieldType_pseudoMetricType : numClosedFieldType >-> pseudoMetricType.
+
+Coercion realFieldType_pointedType : realFieldType >-> pointedType.
+Coercion realFieldType_filteredType : realFieldType >-> filteredType.
+Coercion realFieldType_topologicalType : realFieldType >-> topologicalType.
+Coercion realFieldType_pseudoMetricType : realFieldType >-> pseudoMetricType.
+
+Coercion archiFieldType_pointedType : archiFieldType >-> pointedType.
+Coercion archiFieldType_filteredType : archiFieldType >-> filteredType.
+Coercion archiFieldType_topologicalType : archiFieldType >-> topologicalType.
+Coercion archiFieldType_pseudoMetricType : archiFieldType >-> pseudoMetricType.
+
+Coercion rcfType_pointedType : rcfType >-> pointedType.
+Coercion rcfType_filteredType : rcfType >-> filteredType.
+Coercion rcfType_topologicalType : rcfType >-> topologicalType.
+Coercion rcfType_pseudoMetricType : rcfType >-> pseudoMetricType.
+
+Coercion realType_pointedType : realType >-> pointedType.
+Coercion realType_filteredType : realType >-> filteredType.
+Coercion realType_topologicalType : realType >-> topologicalType.
+Coercion realType_pseudoMetricType : realType >-> pseudoMetricType.
+
+
+End numField_topological.
+
+
+(* Canonical R_pointedType := [pointedType of *)
+(*   Rdefinitions.R for pointed_of_zmodule R_ringType]. *)
+(* (* NB: similar definition in topology.v *) *)
+(* Canonical R_filteredType := [filteredType Rdefinitions.R of *)
+(*   Rdefinitions.R for filtered_of_normedZmod R_normedZmodType]. *)
+(* Canonical R_topologicalType : topologicalType := TopologicalType Rdefinitions.R *)
+(*   (topologyOfBallMixin (pseudoMetric_of_normedDomain R_normedZmodType)). *)
+(* Canonical R_pseudoMetricType : pseudoMetricType R_numDomainType := *)
+(*   PseudoMetricType Rdefinitions.R (pseudoMetric_of_normedDomain R_normedZmodType). *)
+
+Section numFieldType_regular_canonical. (*Modified *)
+  (* TODO: specific module *)
 Variable R : numFieldType.
 (*Canonical topological_of_numFieldType := [numFieldType of R^o].*)
-Canonical numFieldType_pointedType :=
+Canonical numFieldType_regular_pointedType :=
   [pointedType of R^o for pointed_of_zmodule R].
-Canonical numFieldType_filteredType :=
+Canonical numFieldType_regular_filteredType :=
   [filteredType R of R^o for filtered_of_normedZmod R].
-Canonical numFieldType_topologicalType : topologicalType := TopologicalType R^o
+Canonical numFieldType_regular_topologicalType : topologicalType := TopologicalType R^o
   (topologyOfEntourageMixin
     (uniformityOfBallMixin
       (@nbhs_ball_normE _ [normedZmodType R of R])
       (pseudoMetric_of_normedDomain [normedZmodType R of R]))).
-Canonical numFieldType_uniformType : uniformType := UniformType R^o
+Canonical numFieldType_regular_uniformType : uniformType := UniformType R^o
   (uniformityOfBallMixin (@nbhs_ball_normE _ [normedZmodType R of R])
     (pseudoMetric_of_normedDomain [normedZmodType R of R])).
-Canonical numFieldType_pseudoMetricType := @PseudoMetric.Pack R R^o (@PseudoMetric.Class R R
-  (Uniform.class numFieldType_uniformType) (@pseudoMetric_of_normedDomain R R)).
+Canonical numFieldType_regular_pseudoMetricType :=
+  @PseudoMetric.Pack R R^o (@PseudoMetric.Class R R
+  (Uniform.class (numFieldType_uniformType R)) (@pseudoMetric_of_normedDomain R R)).
 Definition numdFieldType_lalgType : lalgType R := @GRing.regular_lalgType R.
-End numFieldType_canonical.
+End numFieldType_regular_canonical.
+
+
 
 Lemma nbhsN (R : numFieldType) (x : R^o) :
   nbhs (- x) = [set [set - y | y in A] | A in nbhs x].
@@ -304,14 +581,14 @@ exists e => // y xe_y; exists (- y); last by rewrite opprK.
 by apply/oppxe_A; rewrite /ball /= distrC opprK addrC.
 Qed.
 
-Lemma openN (R : numFieldType) (A : set R^o) :
+Lemma openN (R : numFieldType) (A : set R) :
   open A -> open [set - x | x in A].
 Proof.
 move=> Aop; rewrite openE => _ [x /Aop x_A <-].
 by rewrite /interior nbhsN; exists A.
 Qed.
 
-Lemma closedN (R : numFieldType) (A : set R^o) :
+Lemma closedN (R : numFieldType) (A : set R) :
   closed A -> closed [set - x | x in A].
 Proof.
 move=> Acl x clNAx.
@@ -452,15 +729,39 @@ Proof. by case: V => ? [? ? ? ? ? ? []]. Qed.
 
 End pseudoMetricnormedzmodule_lemmas.
 
-Section numFieldType_canonical_contd.
-Variable R : numFieldType.
-Lemma R_ball : @ball _ [pseudoMetricType R of R^o] = ball_ (fun x => `| x |).
+Section numFieldType_pseudoMetricNormedZmod. (*modified*)
+
+Lemma R_ball (R : numFieldType) :
+    @ball _ [pseudoMetricType R of R] = ball_ (fun x => `| x |).
 Proof. by []. Qed.
-Definition numFieldType_pseudoMetricNormedZmodMixin :=
-  PseudoMetricNormedZmodule.Mixin R_ball.
-Canonical numFieldType_pseudoMetricNormedZmodType :=
-  @PseudoMetricNormedZmodType R R^o numFieldType_pseudoMetricNormedZmodMixin.
-End numFieldType_canonical_contd.
+Definition numFieldType_pseudoMetricNormedZmodMixin (R : numFieldType):=
+  PseudoMetricNormedZmodule.Mixin (R_ball R).
+Canonical numFieldType_pseudoMetricNormedZmodType (R : numFieldType) :=
+  @PseudoMetricNormedZmodType R R (numFieldType_pseudoMetricNormedZmodMixin R).
+
+(*NEW*)
+Canonical numClosedFieldType_PseudoMetricNormedZmodule (R: numClosedFieldType) := 
+   [pseudoMetricNormedZmodType _ of R for
+   [pseudoMetricNormedZmodType  _ of [numFieldType of R]]].
+
+Canonical archiFieldType_PseudoMetricNormedZmodule (R: archiFieldType) := 
+   [pseudoMetricNormedZmodType _ of R for
+   [pseudoMetricNormedZmodType  _ of [numFieldType of R]]].
+
+Canonical realFieldType_PseudoMetricNormedZmodule (R: realFieldType) :=
+   [pseudoMetricNormedZmodType _ of R for
+   [pseudoMetricNormedZmodType  _ of [numFieldType of R]]].
+
+Canonical rcfType_PseudoMetricNormedZmodule (R: rcfType) :=
+   [pseudoMetricNormedZmodType _ of R for
+   [pseudoMetricNormedZmodType  _ of [numFieldType of R]]].
+
+Canonical realType_PseudoMetricNormedZmodule (R: realType) :=
+   [pseudoMetricNormedZmodType _ of R for
+   [pseudoMetricNormedZmodType  _ of [numFieldType of R]]].
+(*end NEW*)
+
+End numFieldType_pseudoMetricNormedZmod.
 
 (** locally *)
 
@@ -536,12 +837,13 @@ by split=> zxy e /zxy; rewrite [z + _]addrC [_ + x]addrC.
 Qed.
 
 Lemma coord_continuous {K : numFieldType} m n i j :
-  continuous (fun M : 'M[K^o]_(m.+1, n.+1) => M i j).
+  continuous (fun M : 'M[K]_(m.+1, n.+1) => M i j).
 Proof.
 move=> /= M s /= /(nbhs_ballP (M i j)) [e e0 es].
 apply/nbhs_ballP; exists e => //= N MN; exact/es/MN.
 Qed.
 
+
 Global Instance Proper_nbhs'_numFieldType (R : numFieldType) (x : R^o) :
   ProperFilter (nbhs' x).
 Proof.
@@ -552,6 +854,7 @@ rewrite /ball /= opprD addrA subrr distrC subr0 ger0_norm //.
 by rewrite {2}(splitr e%:num) ltr_spaddl.
 Qed.
 
+
 Global Instance Proper_nbhs'_realType (R : realType) (x : R^o) :
   ProperFilter (nbhs' x).
 Proof. exact: Proper_nbhs'_numFieldType. Qed.
@@ -589,7 +892,7 @@ Proof. by exists c; rewrite realE (ltW H) orbT; split => // x /ltW. Qed.
 
 Section ereal_nbhs_instances.
 Context {R : numFieldType}.
-Let R_topologicalType := [topologicalType of R^o].
+(* Let R_topologicalType := [topologicalType of R^o]. *)
 
 Global Instance ereal_nbhs'_filter :
   forall x : {ereal R}, ProperFilter (ereal_nbhs' x).
@@ -747,7 +1050,7 @@ Notation "-oo" := (ninfty_nbhs _) : ring_scope.
 
 Section infty_nbhs_instances.
 Context {R : numFieldType}.
-Let R_topologicalType := [topologicalType of R^o].
+Let R_topologicalType := [topologicalType of R].
 
 Global Instance proper_pinfty_nbhs : ProperFilter (pinfty_nbhs R).
 Proof.
@@ -1728,15 +2031,40 @@ End NormedModule.
 
 Export NormedModule.Exports.
 
-Lemma R_normZ (R : numDomainType) (l : R) (x : R^o) :
+Section normedMod_of_numfield. (* NEW  !*)
+
+(* Lemma R_normZ (R : numDomainType) (l : R) (x : R^o) : *)
+(*   `| l *: x | = `| l | * `| x |. *)
+(* Proof. by rewrite normrM. Qed. *)
+
+(*NB: this is replacing  R_normZ above *)
+Lemma numDomain_normZ (R : numDomainType) (l : R) (x : R^o) :
+  `| l *: x | = `| l | * `| x |.
+Proof. by rewrite normrM. Qed.
+
+Lemma numField_normZ (R : numFieldType) (l : R) (x : R) :
   `| l *: x | = `| l | * `| x |.
 Proof. by rewrite normrM. Qed.
 
 Definition numFieldType_NormedModMixin (R : numFieldType) :=
-  NormedModMixin (@R_normZ R).
+  NormedModMixin (@numField_normZ R).
+
 Canonical numFieldType_normedModType (R : numFieldType) :=
+  NormedModType R R (numFieldType_NormedModMixin R).
+
+(* Definition numField_normedModType (R : numFieldType) := *)
+(*   NormedModType R (numField_lmodType R) (@numField_normedModMixin R). *)
+(* (*the only difference is numField_lmodType above *) *)
+(* Canonical numField_normedModType. *)
+(* Variables (R : numFieldType) (V : normedModType R) (x : R) (w : V). *)
+(* Fail Check (x *: w). *)
+
+Canonical regular_numFieldType_normedModType (R : numFieldType) :=
   NormedModType R R^o (numFieldType_NormedModMixin R).
 
+End normedMod_of_numfield.
+
+
 Section NormedModule_numDomainType.
 Variables (R : numDomainType) (V : normedModType R).
 
@@ -1831,7 +2159,7 @@ Definition self_sub (K : numDomainType) (V W : normedModType K)
 Arguments self_sub {K V W} f x /.
 
 Definition fun1 {T : Type} {K : numFieldType} :
-  T -> [normedModType K of K^o] := fun=> 1.
+  T -> K := fun=> 1.
 Arguments fun1 {T K} x /.
 
 Definition dominated_by {T : Type} {K : numDomainType} {V W : normedModType K}
@@ -2103,7 +2431,7 @@ End NbhsNorm.
 
 Section hausdorff.
 
-Lemma Rhausdorff (R : realFieldType) : hausdorff [topologicalType of R^o].
+Lemma Rhausdorff (R : realFieldType) : hausdorff R. 
 Proof.
 move=> x y clxy; apply/eqP; rewrite eq_le.
 apply/(@in_segment_addgt0Pr _ x _ x) => _ /posnumP[e].
@@ -2644,7 +2972,7 @@ Section matrix_NormedModule.
 Variables (K : numFieldType) (m n : nat).
 
 Lemma mx_norm_ball :
-  @ball _ [pseudoMetricType K of 'M[K^o]_(m.+1, n.+1)] = ball_ (fun x => `| x |).
+  @ball _ [pseudoMetricType K of 'M[K]_(m.+1, n.+1)] = ball_ (fun x => `| x |).
 Proof.
 rewrite /= /normr /= predeq3E => x e y; split.
 - move=> xe_y; rewrite /ball_ mx_normE.
@@ -2664,7 +2992,7 @@ Qed.
 Definition matrix_PseudoMetricNormedZmodMixin :=
   PseudoMetricNormedZmodule.Mixin mx_norm_ball.
 Canonical matrix_pseudoMetricNormedZmodType :=
-  PseudoMetricNormedZmodType K 'M[K^o]_(m.+1, n.+1) matrix_PseudoMetricNormedZmodMixin.
+  PseudoMetricNormedZmodType K 'M[K]_(m.+1, n.+1) matrix_PseudoMetricNormedZmodMixin.
 
 Lemma mx_normZ (l : K) (x : 'M[K]_(m.+1, n.+1)) : `| l *: x | = `| l | * `| x |.
 Proof.
@@ -2677,7 +3005,7 @@ Qed.
 
 Definition matrix_NormedModMixin := NormedModMixin mx_normZ.
 Canonical matrix_normedModType :=
-  NormedModType K 'M[K^o]_(m.+1, n.+1) matrix_NormedModMixin.
+  NormedModType K 'M[K]_(m.+1, n.+1) matrix_NormedModMixin.
 
 End matrix_NormedModule.
 
@@ -2767,15 +3095,21 @@ Arguments cvg_dist2 {_ _ _ F G FF FG}.
 Canonical AbsRing_NormedModType (K : absRingType) :=
   NormedModType K K^o (AbsRing_NormedModMixin _).*)
 
+
+
+
+
 (** Normed vector spaces have some continuous functions *)
 
 (* kludge *)
-Global Instance filter_nbhs (K' : numFieldType) (k : K'^o) :
+
+Global Instance filter_nbhs (K' : numFieldType) (k : K') :
   Filter (nbhs k).
 Proof.
-exact: (@nbhs_filter [topologicalType of K'^o]).
+exact: (@nbhs_filter). 
 Qed.
 
+
 Section NVS_continuity_normedModType.
 Context {K : numFieldType} {V : normedModType K}.
 Local Notation "'+oo'" := (pinfty_nbhs K).
@@ -2787,6 +3121,7 @@ rewrite !near_simpl /=; near=> a b => /=; rewrite opprD addrACA.
 by rewrite normm_lt_split //; [near: a|near: b]; apply: cvg_dist.
 Grab Existential Variables. all: end_near. Qed.
 
+
 Lemma natmul_continuous n : continuous (fun x : V => x *+ n).
 Proof.
 case: n => [|n] x; first exact: cvg_cst.
@@ -2795,7 +3130,8 @@ rewrite -mulrnBl normrMn -mulr_natr -ltr_pdivl_mulr//.
 by near: a; apply: cvg_dist.
 Grab Existential Variables. all: end_near. Qed.
 
-Lemma scale_continuous : continuous (fun z : K^o * V => z.1 *: z.2).
+Lemma scale_continuous : continuous (fun z : K * V => z.1 *: z.2).
+
 Proof.
 move=> [k x]; apply/cvg_distP=> _/posnumP[e].
 rewrite !near_simpl /=; near +oo => M.
@@ -2808,7 +3144,7 @@ rewrite (@distm_lt_split _ _ (k *: z)) // -?(scalerBr, scalerBl) normmZ.
   by apply: cvg_dist; rewrite // mulr_gt0 // ?invr_gt0 ltr_paddl.
 have zM : `|z| <= M by near: z; near: M; apply:cvg_bounded; apply: cvg_refl.
 rewrite (le_lt_trans (ler_pmul _ _ (lexx _) zM)) // ?ltW // -ltr_pdivl_mulr//.
-by near: l; apply: (cvg_dist (_ : K^o)); rewrite // mulr_gt0// invr_gt0.
+by near: l; apply: cvg_dist; rewrite // mulr_gt0// invr_gt0. 
 Grab Existential Variables. all: end_near. Qed.
 
 Arguments scale_continuous _ _ : clear implicits.
@@ -2818,7 +3154,7 @@ Proof.
 by move=> x; apply: (cvg_comp2 (cvg_cst _) cvg_id (scale_continuous (_, _))).
 Qed.
 
-Lemma scalel_continuous (x : V) : continuous (fun k : K^o => k *: x).
+Lemma scalel_continuous (x : V) : continuous (fun k : K => k *: x).
 Proof.
 by move=> k; apply: (cvg_comp2 cvg_id (cvg_cst _) (scale_continuous (_, _))).
 Qed.
@@ -2831,9 +3167,9 @@ Qed.
 
 (** Continuity of norm *)
 
-Lemma norm_continuous : continuous ((@normr _ V) : V -> K^o).
+Lemma norm_continuous : continuous ((@normr _ V) : V -> K).
 Proof.
-move=> x; apply/(@cvg_distP _ [normedModType K of K^o]) => _/posnumP[e] /=.
+move=> x; apply/cvg_distP => _/posnumP[e] /=.
 rewrite !near_simpl; apply/nbhs_normP; exists e%:num => // y Hy.
 by rewrite -ball_normE in Hy; apply/(le_lt_trans (ler_dist_dist _ _)).
 Qed.
@@ -2842,10 +3178,10 @@ End NVS_continuity_normedModType.
 
 Lemma cvg_dist0 {U} {K : numFieldType} {V : normedModType K}
   {F : set (set U)} {FF : Filter F} (f : U -> V) :
-  (fun x => `|f x|) @ F --> (0 : K^o)
+  (fun x => `|f x|) @ F --> (0 : K)
   -> f @ F --> (0 : V).
 Proof.
-move=> /(cvg_dist (_ : K^o)) fx0; apply/cvg_distP => _/posnumP[e].
+move=> /(cvg_dist (_ : K)) fx0; apply/cvg_distP => _/posnumP[e].
 rewrite near_simpl; have := fx0 _ [gt0 of e%:num]; rewrite near_simpl.
 by apply: filterS => x; rewrite !sub0r !normrN [ `|_| ]ger0_norm.
 Qed.
@@ -2854,11 +3190,11 @@ Section NVS_continuity_mul.
 
 Context {K : numFieldType}.
 
-Lemma mul_continuous : continuous (fun z : K^o * K^o => z.1 * z.2).
+Lemma mul_continuous : continuous (fun z : K * K => z.1 * z.2).
 Proof. exact: scale_continuous. Qed.
 
-Lemma inv_continuous x : x != 0 -> {for x, continuous (GRing.inv : K^o -> K^o)}.
-Proof.
+Lemma inv_continuous x : x != 0 -> {for x, continuous (GRing.inv : K -> K)}.
+Proof. 
 move=> x_neq0 /=; apply/cvg_distP => _/posnumP[e]; rewrite !nearE/=; near=> y.
 have y_gt : `|y| > `|x| / 2.
   have /(le_lt_trans (ler_sub_dist _ _)) : `|x - y| < `|x| / 2.
@@ -2879,7 +3215,7 @@ Section cvg_composition.
 
 Context {K : numFieldType} {V : normedModType K} {T : topologicalType}.
 Context (F : set (set T)) {FF : Filter F}.
-Implicit Types (f g : T -> V) (s : T -> K^o) (k : K^o) (x : T) (a b : V).
+Implicit Types (f g : T -> V) (s : T -> K) (k : K) (x : T) (a b : V).
 
 Lemma cvgN f a : f @ F --> a -> (- f) @ F --> - a.
 Proof. by move=> ?; apply: continuous_cvg => //; exact: opp_continuous. Qed.
@@ -2943,10 +3279,10 @@ move=> k_neq0; rewrite propeqE; split => [/(@cvgZr k^-1)|/(@cvgZr k)/cvgP//].
 by under [_ \*: _]funext => x /= do rewrite scalerK//; apply: cvgP.
 Qed.
 
-Lemma cvg_norm f a : f @ F --> a -> `|f x| @[x --> F] --> (`|a| : K^o).
+Lemma cvg_norm f a : f @ F --> a -> `|f x| @[x --> F] --> (`|a| : K).
 Proof. exact: (continuous_cvg _ (@norm_continuous _ _ _)). Qed.
 
-Lemma is_cvg_norm f : cvg (f @ F) -> cvg ((Num.norm \o f : T -> K^o) @ F).
+Lemma is_cvg_norm f : cvg (f @ F) -> cvg ((Num.norm \o f : T -> K) @ F).
 Proof. by have := cvgP _ (cvg_norm _); apply. Qed.
 
 End cvg_composition.
@@ -2955,7 +3291,7 @@ Section cvg_composition_field.
 
 Context {K : numFieldType}  {T : topologicalType}.
 Context (F : set (set T)) {FF : Filter F}.
-Implicit Types (f g : T -> K^o) (a b : K^o).
+Implicit Types (f g : T -> K) (a b : K).
 
 Lemma cvgM f g a b : f @ F --> a -> g @ F --> b -> (f * g) @ F --> a * b.
 Proof. exact: cvgZ. Qed.
@@ -2995,7 +3331,7 @@ Section limit_composition.
 
 Context {K : numFieldType} {V : normedModType K} {T : topologicalType}.
 Context (F : set (set T)) {FF : ProperFilter F}.
-Implicit Types (f g : T -> V) (s : T -> K^o) (k : K^o) (x : T) (a : V).
+Implicit Types (f g : T -> V) (s : T -> K) (k : K) (x : T) (a : V).
 
 Lemma limN f : cvg (f @ F) -> lim (- f @ F) = - lim (f @ F).
 Proof. by move=> ?; apply: cvg_lim => //; apply: cvgN. Qed.
@@ -3019,8 +3355,8 @@ Proof. by move=> ?; apply: cvg_lim => //; apply: cvgZl. Qed.
 Lemma limZr k f : cvg (f @ F) -> lim (k *: f @ F) = k *: lim (f @ F).
 Proof. by move=> ?; apply: cvg_lim => //; apply: cvgZr. Qed.
 
-Lemma lim_norm f : cvg (f @ F) -> lim ((fun x => `|f x| : K^o) @ F) = `|lim (f @ F)|.
-Proof. by move=> ?; apply: (@cvg_lim [topologicalType of K^o]) => //; apply: cvg_norm. Qed.
+Lemma lim_norm f : cvg (f @ F) -> lim ((fun x => `|f x| : K) @ F) = `|lim (f @ F)|.
+Proof. by move=> ?; apply: cvg_lim => //; apply: cvg_norm. Qed.
 
 End limit_composition.
 
@@ -3028,17 +3364,17 @@ Section limit_composition_field.
 
 Context {K : numFieldType}  {T : topologicalType}.
 Context (F : set (set T)) {FF : ProperFilter F}.
-Implicit Types (f g : T -> K^o).
+Implicit Types (f g : T -> K).
 
 Lemma limM f g : cvg (f @ F) -> cvg (g @ F) ->
    lim (f * g @ F) = lim (f @ F) * lim (g @ F).
 Proof.
-by move=> ? ?; apply: (@cvg_lim [topologicalType of K^o]) => //; apply: cvgM.
+by move=> ? ?; apply: cvg_lim => //; apply: cvgM.
 Qed.
 
 Lemma limV f : cvg (f @ F) -> lim (f @ F) != 0 -> lim ((fun x => (f x)^-1) @ F) = (lim (f @ F))^-1.
 Proof.
-by move=> ? ?; apply: (@cvg_lim [topologicalType of K^o]) => //; apply: cvgV.
+by move=> ? ?; apply: cvg_lim => //; apply: cvgV.
 Qed.
 
 End limit_composition_field.
@@ -3046,7 +3382,7 @@ End limit_composition_field.
 Section local_continuity.
 
 Context {K : numFieldType} {V : normedModType K} {T : topologicalType}.
-Implicit Types (f g : T -> V) (s t : T -> K^o) (x : T) (k : K^o) (a : V).
+Implicit Types (f g : T -> V) (s t : T -> K) (x : T) (k : K) (a : V).
 
 Lemma continuousN (f : T -> V) x :
   {for x, continuous f} -> {for x, continuous (fun x => - f x)}.
@@ -3274,8 +3610,9 @@ Export CompleteNormedModule.Exports.
 
 Arguments cvg_distW {_ _ F FF}.
 
+
 Lemma R_complete (R : realType) (F : set (set R^o)) : ProperFilter F -> cauchy F -> cvg F.
-Proof.
+Proof. (*TODO : missing join on complete ?*)
 move=> FF /cauchy_ballP F_cauchy; apply/cvg_ex.
 pose D := \bigcap_(A in F) (down A).
 have /cauchy_ballP /cauchyP /(_ 1) [//|x0 x01] := F_cauchy.
@@ -3289,7 +3626,7 @@ have D_has_sup : has_sup D; first split.
   rewrite -[ball _ _ _]/(_ (_ < _)) ltr_distl ltr_subl_addr => /andP[/ltW].
   by move=> /(le_trans _) yx01 _ /yx01.
 exists (sup D).
-apply: (cvg_distW (_ : R^o)) => /= _ /posnumP[eps]; near=> x.
+apply: cvg_distW => /= _ /posnumP[eps]; near=> x.
 rewrite ler_distl; move/ubP: (sup_upper_bound D_has_sup) => -> //=.
   apply: sup_le_ub => //; first by case: D_has_sup.
   have Fxeps : F (ball_ [eta normr] x (eps)%:num).
@@ -3306,18 +3643,19 @@ by near: y; near: x; apply: nearP_dep; apply: F_cauchy.
 Grab Existential Variables. all: end_near. Qed.
 
 Canonical R_completeType (R : realType) := CompleteType R^o (@R_complete R).
-(* Canonical R_NormedModule := [normedModType R of R^o]. *)
 
 Canonical R_CompleteNormedModule (R : realType) := [completeNormedModType R of R^o].
+(* TODO *)
 
 Section at_left_right.
 Variable R : numFieldType.
 
-Definition at_left (x : R^o) := within (fun u => u < x) (nbhs x).
-Definition at_right (x : R^o) := within (fun u : R => x < u) (nbhs x).
+Definition at_left (x : R) := within (fun u => u < x) (nbhs x).
+Definition at_right (x : R) := within (fun u : R => x < u) (nbhs x).
+
 (* :TODO: We should have filter notation ^- and ^+ for these *)
 
-Global Instance at_right_proper_filter (x : R^o) : ProperFilter (at_right x).
+Global Instance at_right_proper_filter (x : R) : ProperFilter (at_right x).
 Proof.
 apply: Build_ProperFilter' => -[_/posnumP[d] /(_ (x + d%:num / 2))].
 apply; last (by rewrite ltr_addl); rewrite /=.
@@ -3376,23 +3714,26 @@ End cvg_seq_bounded.
 
 Section open_closed_sets.
 Variable R : realFieldType (* TODO: can we generalize to numFieldType? *).
-Implicit Types y : R.
 
-Lemma open_lt y : open [set x : R^o | x < y].
+(* TODO : topology on R *)
+(** Some open sets of [R] *)
+
+Lemma open_lt (y : R) : open [set x : R| x < y].
 Proof.
 move=> x /=; rewrite -subr_gt0 => yDx_gt0; exists (y - x) => // z.
 by rewrite /= distrC ltr_distl addrCA subrr addr0 => /andP[].
 Qed.
 Hint Resolve open_lt : core.
 
-Lemma open_gt y : open [set x : R^o | x > y].
+
+Lemma open_gt (y : R) : open [set x : R | x > y].
 Proof.
 move=> x /=; rewrite -subr_gt0 => xDy_gt0; exists (x - y) => // z.
 by rewrite /= distrC ltr_distl opprB addrCA subrr addr0 => /andP[].
 Qed.
 Hint Resolve open_gt : core.
 
-Lemma open_neq y : open [set x : R^o | x != y].
+Lemma open_neq (y : R) : open [set x : R | x != y].
 Proof.
 rewrite (_ : xpredC _ = [set x | x < y] `|` [set x | x > y] :> set _) /=.
   by apply: openU => //; apply: open_lt.
@@ -3400,21 +3741,25 @@ rewrite predeqE => x /=; rewrite eq_le !leNgt negb_and !negbK orbC.
 by symmetry; apply (rwP orP).
 Qed.
 
-Lemma closed_le y : closed [set x : R^o | x <= y].
+(** Some closed sets of [R] *)
+
+Lemma closed_le (y : R) : closed [set x : R | x <= y].
 Proof.
 rewrite (_ : [set x | x <= _] = ~` (> y) :> set _).
   by apply: closedC; exact: open_gt.
 by rewrite predeqE => x /=; rewrite leNgt; split => /negP.
 Qed.
 
-Lemma closed_ge y : closed [set x : R^o | y <= x].
+
+Lemma closed_ge (y : R) : closed [set x : R | y <= x].
 Proof.
 rewrite (_ : (>= _) = ~` [set x | x < y] :> set _).
   by apply: closedC; exact: open_lt.
 by rewrite predeqE => x /=; rewrite leNgt; split => /negP.
 Qed.
 
-Lemma closed_eq y : closed [set x : R^o | x = y].
+
+Lemma closed_eq (y : R) : closed [set x : R | x = y].
 Proof.
 rewrite [X in closed X](_ : (eq^~ _) = ~` (xpredC (eq_op^~ y))).
   by apply: closedC; exact: open_neq.
@@ -3435,7 +3780,7 @@ Variable R : realType.
 
 (** properties of segments in [R] *)
 
-Lemma segment_connected (a b : R) : connected [set x : R^o | x \in `[a, b]].
+Lemma segment_connected (a b : R) : connected [set x | x \in `[a, b]].
 Proof.
 move=> A [y Ay] Aop Acl.
 move: Aop; apply: contraPP; rewrite predeqE => /asboolPn /existsp_asboolPn [x].
@@ -3513,14 +3858,14 @@ apply: le_trans; rewrite -ler_subr_addl le_minl; apply/orP; right.
 by rewrite ler_pdivr_mulr // mulrDr mulr1 ler_addl; apply: ltW.
 Qed.
 
-Lemma segment_closed (a b : R) : closed [set x : R^o | x \in `[a, b]].
+Lemma segment_closed (a b : R) : closed [set x | x \in `[a, b]].
 Proof.
 have -> : [set x | x \in `[a, b]] = [set x | x >= a] `&` [set x | x <= b].
   by rewrite predeqE => ?; rewrite inE; split=> [/andP [] | /= [->]].
 by apply closedI; [apply closed_ge | apply closed_le].
 Qed.
 
-Lemma segment_compact (a b : R) : compact [set x : R^o | x \in `[a, b]].
+Lemma segment_compact (a b : R) : compact [set x | x \in `[a, b]].
 Proof.
 case: (lerP a b) => [leab|ltba]; last first.
   by move=> F FF /filter_ex [x abx]; move: ltba; rewrite (itvP abx).
@@ -3583,7 +3928,7 @@ rewrite {1}(splitr x) ger_addl pmulr_lle0 // => /(lt_le_trans x0);
   by rewrite ltxx.
 Qed.
 
-Lemma IVT (R : realType) (f : R^o -> R^o) (a b v : R^o) :
+Lemma IVT (R : realType) (f : R -> R) (a b v : R) :
   a <= b -> {in `[a, b], continuous f} ->
   minr (f a) (f b) <= v <= maxr (f a) (f b) ->
   exists2 c, c \in `[a, b] & f c = v.
@@ -3663,7 +4008,7 @@ move=> [:wlog]; case: a b => [a||] [b||] //= ltax ltxb.
 Qed.
 
 (* TODO: generalize to numFieldType? *)
-Lemma nbhs_interval (R : realFieldType) (P : R -> Prop) (x : R^o) (a b : {ereal R}) :
+Lemma nbhs_interval (R : realFieldType) (P : R -> Prop) (x : R) (a b : {ereal R}) :
   (a < x%:E)%E -> (x%:E < b)%E ->
   (forall y : R, a < y%:E -> y%:E < b -> P y)%E ->
   nbhs x P.
@@ -3899,16 +4244,16 @@ have GC : G [set g | C (\row_j g j)] by exists C.
 by have [g []] := clGf _ _ GC f_D; exists (\row_j (g j : T)).
 Qed.
 
-Lemma bounded_closed_compact (R : realType) n (A : set 'rV[R^o]_n.+1) :
+Lemma bounded_closed_compact (R : realType) n (A : set 'rV[R]_n.+1) :
   bounded_set A -> closed A -> compact A.
 Proof.
 move=> [M [Mreal normAltM]] Acl.
 have Mnco : compact
-  [set v : 'rV[R^o]_n.+1 | (forall i, (v ord0 i) \in `[(- (M + 1)), (M + 1)])].
-  apply: (@rV_compact [topologicalType of R^o] _ (fun _ => [set x | x \in `[(- (M + 1)), (M + 1)]])).
+  [set v : 'rV[R]_n.+1 | (forall i, (v ord0 i) \in `[(- (M + 1)), (M + 1)])].
+  apply: (@rV_compact _  _ (fun _ => [set x | x \in `[(- (M + 1)), (M + 1)]])).
   by move=> _; apply: segment_compact.
 apply: subclosed_compact Acl Mnco _ => v /normAltM normvleM i.
-suff : `|v ord0 i : R^o| <= M + 1 by rewrite ler_norml.
+suff : `|v ord0 i : R| <= M + 1 by rewrite ler_norml.
 apply: le_trans (normvleM _ _); last by rewrite ltr_addl.
 have /mapP[j Hj ->] : `|v ord0 i| \in [seq `|v ij.1 ij.2| | ij : 'I_1 * 'I_n.+1].
   by apply/mapP; exists (ord0, i) => //=; rewrite mem_enum.
@@ -3934,7 +4279,7 @@ Variable R : realFieldType (* TODO: generalize to numFieldType? *).
 Implicit Types x y : {ereal R}.
 Implicit Types r : R.
 
-Lemma open_ereal_lt y : open [set r : R^o | r%:E < y]%E.
+Lemma open_ereal_lt y : open [set r : R | r%:E < y]%E.
 Proof.
 case: y => [y||] /=; first exact: open_lt.
 rewrite [X in open X](_ : _ = setT); first exact: openT.
@@ -3943,7 +4288,7 @@ rewrite [X in open X](_ : _ = set0); first exact: open0.
 by rewrite funeqE => ?; rewrite falseE.
 Qed.
 
-Lemma open_ereal_gt y : open [set r : R^o | y < r%:E]%E.
+Lemma open_ereal_gt y : open [set r : R | y < r%:E]%E.
 Proof.
 case: y => [y||] /=; first exact: open_gt.
 rewrite [X in open X](_ : _ = set0); first exact: open0.
@@ -4029,7 +4374,7 @@ Section ereal_is_hausdorff.
 Variable R : realFieldType.
 Implicit Types r : R.
 
-Lemma nbhs_image_ERFin (x : R^o) (X : set R) :
+Lemma nbhs_image_ERFin (x : R) (X : set R) :
   nbhs x X -> nbhs x%:E ((fun r => r%:E) @` X).
 Proof.
 case => _/posnumP[e] xeX; exists e%:num => //= r xer.
@@ -4147,3 +4492,4 @@ rewrite !nbhs_nearE !near_map !near_nbhs in fxP *; have /= := cfx P fxP.
 rewrite !near_simpl near_withinE near_simpl => Pf; near=> y.
 by have [->|] := eqVneq y x; [by apply: nbhs_singleton|near: y].
 Grab Existential Variables. all: end_near. Qed.
+