Merge remote-tracking branch 'upstream/master' into fixdoc

17 files changed, 781 insertions, 41 deletions

diff --git a/mathcomp/algebra/finalg.v b/mathcomp/algebra/finalg.v
index 1c98465..0cf29b2 100644
--- a/mathcomp/algebra/finalg.v
+++ b/mathcomp/algebra/finalg.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
diff --git a/mathcomp/algebra/fraction.v b/mathcomp/algebra/fraction.v
index cfa13ed..8cf811a 100644
--- a/mathcomp/algebra/fraction.v
+++ b/mathcomp/algebra/fraction.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v
index 2871ff5..7c99443 100644
--- a/mathcomp/algebra/intdiv.v
+++ b/mathcomp/algebra/intdiv.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v
index 6806094..56dec94 100644
--- a/mathcomp/algebra/interval.v
+++ b/mathcomp/algebra/interval.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index 4469266..2aa117d 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index a0fa1c6..3b3ca5d 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v
index f64ad9a..1301a94 100644
--- a/mathcomp/algebra/mxpoly.v
+++ b/mathcomp/algebra/mxpoly.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index 1209289..22caa4a 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
@@ -2541,6 +2541,32 @@ Definition prim_rootP := prim_rootP.
 
 End UnityRootTheory.
 
+Section DecField.
+
+Variable F : decFieldType.
+
+Lemma dec_factor_theorem (p : {poly F}) :
+  {s : seq F & {q : {poly F} | p = q * \prod_(x <- s) ('X - x%:P)
+                             /\ (q != 0 -> forall x, ~~ root q x)}}.
+Proof.
+pose polyT (p : seq F) := (foldr (fun c f => f * 'X_0 + c%:T) (0%R)%:T p)%T.
+have eval_polyT (q : {poly F}) x : GRing.eval [:: x] (polyT q) = q.[x].
+  by rewrite /horner; elim: (val q) => //= ? ? ->.
+elim: size {-2}p (leqnn (size p)) => {p} [p|n IHn p].
+  by move=> /size_poly_leq0P->; exists [::], 0; rewrite mul0r eqxx.
+have /decPcases /= := @satP F [::] ('exists 'X_0, polyT p == 0%T).
+case: ifP => [_ /sig_eqW[x]|_ noroot]; last first.
+  exists [::], p; rewrite big_nil mulr1; split => // p_neq0 x.
+  by apply/negP=> /rootP rpx; apply noroot; exists x; rewrite eval_polyT.
+rewrite eval_polyT => /rootP /factor_theorem /sig_eqW [q ->].
+have [->|q_neq0] := eqVneq q 0; first by exists [::], 0; rewrite !mul0r eqxx.
+rewrite size_mul ?polyXsubC_eq0 // ?size_XsubC addn2 /= ltnS => sq_le_n.
+have [] // := IHn q => s [r [-> nr]]; exists (s ++ [::x]), r.
+by rewrite big_cat /= big_seq1 mulrA.
+Qed.
+
+End DecField.
+
 Module PreClosedField.
 Section UseAxiom.
 
@@ -2590,15 +2616,12 @@ Proof. exact: PreClosedField.closed_nonrootP. Qed.
 Lemma closed_field_poly_normal p :
   {r : seq F | p = lead_coef p *: \prod_(z <- r) ('X - z%:P)}.
 Proof.
-apply: sig_eqW; elim: {p}_.+1 {-2}p (ltnSn (size p)) => // n IHn p le_p_n.
-have [/size1_polyC-> | p_gt1] := leqP (size p) 1.
-  by exists nil; rewrite big_nil lead_coefC alg_polyC.
-have [|x /factor_theorem[q Dp]] := closed_rootP p _; first by rewrite gtn_eqF.
-have nz_p: p != 0 by rewrite -size_poly_eq0 -(subnKC p_gt1).
-have:= nz_p; rewrite Dp mulf_eq0 lead_coefM => /norP[nz_q nz_Xx].
-rewrite ltnS polySpred // Dp size_mul // size_XsubC addn2 in le_p_n.
-have [r {1}->] := IHn q le_p_n; exists (x :: r).
-by rewrite lead_coefXsubC mulr1 big_cons -scalerAl mulrC.
+apply: sig_eqW; have [r [q [->]]] /= := dec_factor_theorem p.
+have [->|] := altP eqP; first by exists [::]; rewrite mul0r lead_coef0 scale0r.
+have [[x rqx ? /(_ isT x) /negP /(_ rqx)] //|] := altP (closed_rootP q).
+rewrite negbK => /size_poly1P [c c_neq0-> _ _]; exists r.
+rewrite mul_polyC lead_coefZ (monicP _) ?mulr1 //.
+by rewrite monic_prod => // i; rewrite monicXsubC.
 Qed.
 
 End ClosedField.
diff --git a/mathcomp/algebra/polyXY.v b/mathcomp/algebra/polyXY.v
index a2acd5f..82a4afb 100644
--- a/mathcomp/algebra/polyXY.v
+++ b/mathcomp/algebra/polyXY.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v
index 1782d95..b5e1068 100644
--- a/mathcomp/algebra/polydiv.v
+++ b/mathcomp/algebra/polydiv.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v
index 9012291..d004748 100644
--- a/mathcomp/algebra/rat.v
+++ b/mathcomp/algebra/rat.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
@@ -11,8 +11,6 @@ Require Import bigop ssralg div ssrnum ssrint.
 (* structure of archimedean, real field, with int and nat declared as closed  *)
 (* subrings.                                                                  *)
 (*          rat == the type of rational number, with single constructor Rat   *)
-(*      Rat p h == the element of type rat build from p a pair of integers and*)
-(*                 h a proof of (0 < p.2) && coprime `|p.1| `|p.2|            *)
 (*         n%:Q == explicit cast from int to rat, postfix notation for the    *)
 (*                 ratz constant                                              *)
 (*       numq r == numerator of (r : rat)                                     *)
diff --git a/mathcomp/algebra/ring_quotient.v b/mathcomp/algebra/ring_quotient.v
index 1b9433e..8d8eaaf 100644
--- a/mathcomp/algebra/ring_quotient.v
+++ b/mathcomp/algebra/ring_quotient.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index a494f3f..9d93608 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
@@ -5107,6 +5107,12 @@ Variable F : closedFieldType.
 Lemma solve_monicpoly : ClosedField.axiom F.
 Proof. by case: F => ? []. Qed.
 
+Lemma imaginary_exists : {i : F | i ^+ 2 = -1}.
+Proof.
+have /sig_eqW[i Di2] := @solve_monicpoly 2 (nth 0 [:: -1]) isT.
+by exists i; rewrite Di2 !big_ord_recl big_ord0 mul0r mulr1 !addr0.
+Qed.
+
 End ClosedFieldTheory.
 
 Module SubType.
@@ -5741,6 +5747,7 @@ Definition rmorph_alg := rmorph_alg.
 Definition lrmorphismP := lrmorphismP.
 Definition can2_lrmorphism := can2_lrmorphism.
 Definition bij_lrmorphism := bij_lrmorphism.
+Definition imaginary_exists := imaginary_exists.
 
 Notation null_fun V := (null_fun V) (only parsing).
 Notation in_alg A := (in_alg_loc A).
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index a8b9a04..eb66940 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index b1c1746..219f804 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -1,8 +1,8 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
-Require Import ssrfun ssrbool eqtype ssrnat seq div choice fintype.
+Require Import ssrfun ssrbool eqtype ssrnat seq div choice fintype path.
 From mathcomp
 Require Import bigop ssralg finset fingroup zmodp poly.
 
@@ -60,17 +60,24 @@ Require Import bigop ssralg finset fingroup zmodp poly.
 (*                  == clone of a canonical archiFieldType structure on T     *)
 (*                                                                            *)
 (*   * RealClosedField (Real Field with the real closed axiom)                *)
-(*    realClosedFieldType                                                     *)
-(*                  == interface for a real closed field.                     *)
-(*   RealClosedFieldType T r                                                  *)
-(*                  == packs the real closed axiom r into a                   *)
-(*                     realClodedFieldType. The  carrier T must have a real   *)
+(*    rcfType       == interface for a real closed field.                     *)
+(*   RcfType T r    == packs the real closed axiom r into a                   *)
+(*                     rcfType. The  carrier T must have a real               *)
 (*                     field type structure.                                  *)
-(*  [realClosedFieldType of T for S ]                                         *)
-(*                  == T-clone of the realClosedFieldType structure  S.       *)
-(*  [realClosedFieldype of T]                                                 *)
-(*                  == clone of a canonical realClosedFieldType structure on  *)
+(*  [rcfType of T]  == clone of a canonical realClosedFieldType structure on  *)
 (*                     T.                                                     *)
+(*  [rcfType of T for S ]                                                     *)
+(*                  == T-clone of the realClosedFieldType structure  S.       *)
+(*                                                                            *)
+(*   * NumClosedField (Partially ordered Closed Field with conjugation)       *)
+(*    numClosedFieldType       == interface for a closed field with conj.     *)
+(*  NumClosedFieldType T r    == packs the real closed axiom r into a         *)
+(*                     numClosedFieldType. The  carrier T must have a closed  *)
+(*                     field type structure.                                  *)
+(*  [numClosedFieldType of T]  == clone of a canonical numClosedFieldType     *)
+(*                               structure on  T                              *)
+(*  [numClosedFieldType of T for S ]                                          *)
+(*                  == T-clone of the realClosedFieldType structure  S.       *)
 (*                                                                            *)
 (* Over these structures, we have the following operations                    *)
 (*            `|x| == norm of x.                                              *)
@@ -89,6 +96,18 @@ Require Import bigop ssralg finset fingroup zmodp poly.
 (*                     and n such that `|x| < n%:R.                           *)
 (*       Num.sqrt x == in a real-closed field, a positive square root of x if *)
 (*                     x >= 0, or 0 otherwise.                                *)
+(* For numeric algebraically closed fields we provide the generic definitions *)
+(*         'i == the imaginary number (:= sqrtC (-1)).                        *)
+(*      'Re z == the real component of z.                                     *)
+(*      'Im z == the imaginary component of z.                                *)
+(*        z^* == the complex conjugate of z (:= conjC z).                     *)
+(*    sqrtC z == a nonnegative square root of z, i.e., 0 <= sqrt x if 0 <= x. *)
+(*  n.-root z == more generally, for n > 0, an nth root of z, chosen with a   *)
+(*               minimal non-negative argument for n > 1 (i.e., with a        *)
+(*               maximal real part subject to a nonnegative imaginary part).  *)
+(*               Note that n.-root (-1) is a primitive 2nth root of unity,    *)
+(*               an thus not equal to -1 for n odd > 1 (this will be shown in *)
+(*               file cyclotomic.v).                                          *)
 (*                                                                            *)
 (*  There are now three distinct uses of the symbols <, <=, > and >=:         *)
 (*    0-ary, unary (prefix) and binary (infix).                               *)
@@ -401,9 +420,17 @@ Module ClosedField.
 
 Section ClassDef.
 
+Record imaginary_mixin_of (R : numDomainType) := ImaginaryMixin {
+  imaginary : R;
+  conj_op : {rmorphism R -> R};
+  _ : imaginary ^+ 2 = - 1;
+  _ : forall x, x * conj_op x = `|x| ^+ 2;
+}.
+
 Record class_of R := Class {
   base : GRing.ClosedField.class_of R;
-  mixin : mixin_of (ring_for R base)
+  mixin : mixin_of (ring_for R base);
+  conj_mixin : imaginary_mixin_of (num_for R (NumDomain.Class mixin))
 }.
 Definition base2 R (c : class_of R) := NumField.Class (mixin c).
 Local Coercion base : class_of >-> GRing.ClosedField.class_of.
@@ -419,7 +446,8 @@ Definition pack :=
   fun bT b & phant_id (GRing.ClosedField.class bT)
                       (b : GRing.ClosedField.class_of T) =>
   fun mT m & phant_id (NumField.class mT) (@NumField.Class T b m) =>
-  Pack (@Class T b m) T.
+  fun mc => Pack (@Class T b m mc) T.
+Definition clone := fun b & phant_id class (b : class_of T) => Pack b T.
 
 Definition eqType := @Equality.Pack cT xclass xT.
 Definition choiceType := @Choice.Pack cT xclass xT.
@@ -431,6 +459,7 @@ Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
 Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
 Definition numDomainType := @NumDomain.Pack cT xclass xT.
 Definition fieldType := @GRing.Field.Pack cT xclass xT.
+Definition numFieldType := @NumField.Pack cT xclass xT.
 Definition decFieldType := @GRing.DecidableField.Pack cT xclass xT.
 Definition closedFieldType := @GRing.ClosedField.Pack cT xclass xT.
 Definition join_dec_numDomainType := @NumDomain.Pack decFieldType xclass xT.
@@ -467,6 +496,8 @@ Coercion fieldType : type >-> GRing.Field.type.
 Canonical fieldType.
 Coercion decFieldType : type >-> GRing.DecidableField.type.
 Canonical decFieldType.
+Coercion numFieldType : type >-> NumField.type.
+Canonical numFieldType.
 Coercion closedFieldType : type >-> GRing.ClosedField.type.
 Canonical closedFieldType.
 Canonical join_dec_numDomainType.
@@ -474,7 +505,11 @@ Canonical join_dec_numFieldType.
 Canonical join_numDomainType.
 Canonical join_numFieldType.
 Notation numClosedFieldType := type.
-Notation "[ 'numClosedFieldType' 'of' T ]" := (@pack T _ _ id _ _ id)
+Notation NumClosedFieldType T m := (@pack T _ _ id _ _ id m).
+Notation "[ 'numClosedFieldType' 'of' T 'for' cT ]" := (@clone T cT _ id)
+  (at level 0, format "[ 'numClosedFieldType'  'of'  T  'for' cT ]") :
+                                                         form_scope.
+Notation "[ 'numClosedFieldType' 'of' T ]" := (@clone T _ _ id)
   (at level 0, format "[ 'numClosedFieldType'  'of'  T ]") : form_scope.
 End Exports.
 
@@ -4085,6 +4120,682 @@ Qed.
 
 End RealClosedFieldTheory.
 
+Definition conjC {C : numClosedFieldType} : {rmorphism C -> C} :=
+ ClosedField.conj_op (ClosedField.conj_mixin (ClosedField.class C)).
+Notation "z ^*" := (@conjC _ z) (at level 2, format "z ^*") : ring_scope.
+
+Definition imaginaryC {C : numClosedFieldType} : C :=
+ ClosedField.imaginary (ClosedField.conj_mixin (ClosedField.class C)).
+Notation "'i" := (@imaginaryC _) (at level 0) : ring_scope.
+
+Section ClosedFieldTheory.
+
+Variable C : numClosedFieldType.
+Implicit Types a x y z : C.
+
+Definition normCK x : `|x| ^+ 2 = x * x^*.
+Proof. by case: C x => ? [? ? []]. Qed.
+
+Lemma sqrCi : 'i ^+ 2 = -1 :> C.
+Proof. by case: C => ? [? ? []]. Qed.
+
+Lemma conjCK : involutive (@conjC C).
+Proof.
+have JE x : x^* = `|x|^+2 / x.
+  have [->|x_neq0] := eqVneq x 0; first by rewrite rmorph0 invr0 mulr0.
+  by apply: (canRL (mulfK _)) => //; rewrite mulrC -normCK.
+move=> x; have [->|x_neq0] := eqVneq x 0; first by rewrite !rmorph0.
+rewrite !JE normrM normfV exprMn normrX normr_id.
+rewrite invfM exprVn mulrA -[X in X * _]mulrA -invfM -exprMn.
+by rewrite divff ?mul1r ?invrK // !expf_eq0 normr_eq0 //.
+Qed.
+
+Let Re2 z := z + z^*.
+Definition nnegIm z := (0 <= imaginaryC * (z^* - z)).
+Definition argCle y z := nnegIm z ==> nnegIm y && (Re2 z <= Re2 y).
+
+CoInductive rootC_spec n (x : C) : Type :=
+  RootCspec (y : C) of if (n > 0)%N then y ^+ n = x else y = 0
+                        & forall z, (n > 0)%N -> z ^+ n = x -> argCle y z.
+
+Fact rootC_subproof n x : rootC_spec n x.
+Proof.
+have realRe2 u : Re2 u \is Num.real.
+  rewrite realEsqr expr2 {2}/Re2 -{2}[u]conjCK addrC -rmorphD -normCK.
+  by rewrite exprn_ge0 ?normr_ge0.
+have argCle_total : total argCle.
+  move=> u v; rewrite /total /argCle.
+  by do 2!case: (nnegIm _) => //; rewrite ?orbT //= real_leVge.
+have argCle_trans : transitive argCle.
+  move=> u v w /implyP geZuv /implyP geZvw; apply/implyP.
+  by case/geZvw/andP=> /geZuv/andP[-> geRuv] /ler_trans->.
+pose p := 'X^n - (x *+ (n > 0))%:P; have [r0 Dp] := closed_field_poly_normal p.
+have sz_p: size p = n.+1.
+  rewrite size_addl ?size_polyXn // ltnS size_opp size_polyC mulrn_eq0.
+  by case: posnP => //; case: negP.
+pose r := sort argCle r0; have r_arg: sorted argCle r by apply: sort_sorted.
+have{Dp} Dp: p = \prod_(z <- r) ('X - z%:P).
+  rewrite Dp lead_coefE sz_p coefB coefXn coefC -mulrb -mulrnA mulnb lt0n andNb.
+  rewrite subr0 eqxx scale1r; apply: eq_big_perm.
+  by rewrite perm_eq_sym perm_sort.
+have mem_rP z: (n > 0)%N -> reflect (z ^+ n = x) (z \in r).
+  move=> n_gt0; rewrite -root_prod_XsubC -Dp rootE !hornerE hornerXn n_gt0.
+  by rewrite subr_eq0; apply: eqP.
+exists r`_0 => [|z n_gt0 /(mem_rP z n_gt0) r_z].
+  have sz_r: size r = n by apply: succn_inj; rewrite -sz_p Dp size_prod_XsubC.
+  case: posnP => [n0 | n_gt0]; first by rewrite nth_default // sz_r n0.
+  by apply/mem_rP=> //; rewrite mem_nth ?sz_r.
+case: {Dp mem_rP}r r_z r_arg => // y r1; rewrite inE => /predU1P[-> _|r1z].
+  by apply/implyP=> ->; rewrite lerr.
+by move/(order_path_min argCle_trans)/allP->.
+Qed.
+
+Definition nthroot n x := let: RootCspec y _ _ := rootC_subproof n x in y.
+Notation "n .-root" := (nthroot n) (at level 2, format "n .-root") : ring_core_scope.
+Notation "n .-root" := (nthroot n) (only parsing) : ring_scope.
+Notation sqrtC := 2.-root.
+
+Definition Re x := (x + x^*) / 2%:R.
+Definition Im x := 'i * (x^* - x) / 2%:R.
+Notation "'Re z" := (Re z) (at level 10, z at level 8) : ring_scope.
+Notation "'Im z" := (Im z) (at level 10, z at level 8) : ring_scope.
+
+Let nz2 : 2%:R != 0 :> C. Proof. by rewrite pnatr_eq0. Qed.
+
+Lemma normCKC x : `|x| ^+ 2 = x^* * x. Proof. by rewrite normCK mulrC. Qed.
+
+Lemma mul_conjC_ge0 x : 0 <= x * x^*.
+Proof. by rewrite -normCK exprn_ge0 ?normr_ge0. Qed.
+
+Lemma mul_conjC_gt0 x : (0 < x * x^*) = (x != 0).
+Proof.
+have [->|x_neq0] := altP eqP; first by rewrite rmorph0 mulr0.
+by rewrite -normCK exprn_gt0 ?normr_gt0.
+Qed.
+
+Lemma mul_conjC_eq0 x : (x * x^* == 0) = (x == 0).
+Proof. by rewrite -normCK expf_eq0 normr_eq0. Qed.
+
+Lemma conjC_ge0 x : (0 <= x^*) = (0 <= x).
+Proof.
+wlog suffices: x / 0 <= x -> 0 <= x^*.
+  by move=> IH; apply/idP/idP=> /IH; rewrite ?conjCK.
+rewrite le0r => /predU1P[-> | x_gt0]; first by rewrite rmorph0.
+by rewrite -(pmulr_rge0 _ x_gt0) mul_conjC_ge0.
+Qed.
+
+Lemma conjC_nat n : (n%:R)^* = n%:R :> C. Proof. exact: rmorph_nat. Qed.
+Lemma conjC0 : 0^* = 0 :> C. Proof. exact: rmorph0. Qed.
+Lemma conjC1 : 1^* = 1 :> C. Proof. exact: rmorph1. Qed.
+Lemma conjC_eq0 x : (x^* == 0) = (x == 0). Proof. exact: fmorph_eq0. Qed.
+
+Lemma invC_norm x : x^-1 = `|x| ^- 2 * x^*.
+Proof.
+have [-> | nx_x] := eqVneq x 0; first by rewrite conjC0 mulr0 invr0.
+by rewrite normCK invfM divfK ?conjC_eq0.
+Qed.
+
+(* Real number subset. *)
+
+Lemma CrealE x : (x \is real) = (x^* == x).
+Proof.
+rewrite realEsqr ger0_def normrX normCK.
+by have [-> | /mulfI/inj_eq-> //] := eqVneq x 0; rewrite rmorph0 !eqxx.
+Qed.
+
+Lemma CrealP {x} : reflect (x^* = x) (x \is real).
+Proof. by rewrite CrealE; apply: eqP. Qed.
+
+Lemma conj_Creal x : x \is real -> x^* = x.
+Proof. by move/CrealP. Qed.
+
+Lemma conj_normC z : `|z|^* = `|z|.
+Proof. by rewrite conj_Creal ?normr_real. Qed.
+
+Lemma geC0_conj x : 0 <= x -> x^* = x.
+Proof. by move=> /ger0_real/CrealP. Qed.
+
+Lemma geC0_unit_exp x n : 0 <= x -> (x ^+ n.+1 == 1) = (x == 1).
+Proof. by move=> x_ge0; rewrite pexpr_eq1. Qed.
+
+(* Elementary properties of roots. *)
+
+Ltac case_rootC := rewrite /nthroot; case: (rootC_subproof _ _).
+
+Lemma root0C x : 0.-root x = 0. Proof. by case_rootC. Qed.
+
+Lemma rootCK n : (n > 0)%N -> cancel n.-root (fun x => x ^+ n).
+Proof. by case: n => //= n _ x; case_rootC. Qed.
+
+Lemma root1C x : 1.-root x = x. Proof. exact: (@rootCK 1). Qed.
+
+Lemma rootC0 n : n.-root 0 = 0.
+Proof.
+have [-> | n_gt0] := posnP n; first by rewrite root0C.
+by have /eqP := rootCK n_gt0 0; rewrite expf_eq0 n_gt0 /= => /eqP.
+Qed.
+
+Lemma rootC_inj n : (n > 0)%N -> injective n.-root.
+Proof. by move/rootCK/can_inj. Qed.
+
+Lemma eqr_rootC n : (n > 0)%N -> {mono n.-root : x y / x == y}.
+Proof. by move/rootC_inj/inj_eq. Qed.
+
+Lemma rootC_eq0 n x : (n > 0)%N -> (n.-root x == 0) = (x == 0).
+Proof. by move=> n_gt0; rewrite -{1}(rootC0 n) eqr_rootC. Qed.
+
+(* Rectangular coordinates. *)
+
+Lemma nonRealCi : ('i : C) \isn't real.
+Proof. by rewrite realEsqr sqrCi oppr_ge0 ltr_geF ?ltr01. Qed.
+
+Lemma neq0Ci : 'i != 0 :> C.
+Proof. by apply: contraNneq nonRealCi => ->; apply: real0. Qed.
+
+Lemma normCi : `|'i| = 1 :> C.
+Proof.
+apply/eqP; rewrite -(@pexpr_eq1 _ _ 2) ?normr_ge0 //.
+by rewrite -normrX sqrCi normrN1.
+Qed.
+
+Lemma invCi : 'i^-1 = - 'i :> C.
+Proof. by rewrite -div1r -[1]opprK -sqrCi mulNr mulfK ?neq0Ci. Qed.
+
+Lemma conjCi : 'i^* = - 'i :> C.
+Proof. by rewrite -invCi invC_norm normCi expr1n invr1 mul1r. Qed.
+
+Lemma Crect x : x = 'Re x + 'i * 'Im x.
+Proof.
+rewrite 2!mulrA -expr2 sqrCi mulN1r opprB -mulrDl addrACA subrr addr0.
+by rewrite -mulr2n -mulr_natr mulfK.
+Qed.
+
+Lemma Creal_Re x : 'Re x \is real.
+Proof. by rewrite CrealE fmorph_div rmorph_nat rmorphD conjCK addrC. Qed.
+
+Lemma Creal_Im x : 'Im x \is real.
+Proof.
+rewrite CrealE fmorph_div rmorph_nat rmorphM rmorphB conjCK.
+by rewrite conjCi -opprB mulrNN.
+Qed.
+Hint Resolve Creal_Re Creal_Im.
+
+Fact Re_is_additive : additive Re.
+Proof. by move=> x y; rewrite /Re rmorphB addrACA -opprD mulrBl. Qed.
+Canonical Re_additive := Additive Re_is_additive.
+
+Fact Im_is_additive : additive Im.
+Proof.
+by move=> x y; rewrite /Im rmorphB opprD addrACA -opprD mulrBr mulrBl.
+Qed.
+Canonical Im_additive := Additive Im_is_additive.
+
+Lemma Creal_ImP z : reflect ('Im z = 0) (z \is real).
+Proof.
+rewrite CrealE -subr_eq0 -(can_eq (mulKf neq0Ci)) mulr0.
+by rewrite -(can_eq (divfK nz2)) mul0r; apply: eqP.
+Qed.
+
+Lemma Creal_ReP z : reflect ('Re z = z) (z \in real).
+Proof.
+rewrite (sameP (Creal_ImP z) eqP) -(can_eq (mulKf neq0Ci)) mulr0.
+by rewrite -(inj_eq (addrI ('Re z))) addr0 -Crect eq_sym; apply: eqP.
+Qed.
+
+Lemma ReMl : {in real, forall x, {morph Re : z / x * z}}.
+Proof.
+by move=> x Rx z /=; rewrite /Re rmorphM (conj_Creal Rx) -mulrDr -mulrA.
+Qed.
+
+Lemma ReMr : {in real, forall x, {morph Re : z / z * x}}.
+Proof. by move=> x Rx z /=; rewrite mulrC ReMl // mulrC. Qed.
+
+Lemma ImMl : {in real, forall x, {morph Im : z / x * z}}.
+Proof.
+by move=> x Rx z; rewrite /Im rmorphM (conj_Creal Rx) -mulrBr mulrCA !mulrA.
+Qed.
+
+Lemma ImMr : {in real, forall x, {morph Im : z / z * x}}.
+Proof. by move=> x Rx z /=; rewrite mulrC ImMl // mulrC. Qed.
+
+Lemma Re_i : 'Re 'i = 0. Proof. by rewrite /Re conjCi subrr mul0r. Qed.
+
+Lemma Im_i : 'Im 'i = 1.
+Proof.
+rewrite /Im conjCi -opprD mulrN -mulr2n mulrnAr ['i * _]sqrCi.
+by rewrite mulNrn opprK divff.
+Qed.
+
+Lemma Re_conj z : 'Re z^* = 'Re z.
+Proof. by rewrite /Re addrC conjCK. Qed.
+
+Lemma Im_conj z : 'Im z^* = - 'Im z.
+Proof. by rewrite /Im -mulNr -mulrN opprB conjCK. Qed.
+
+Lemma Re_rect : {in real &, forall x y, 'Re (x + 'i * y) = x}.
+Proof.
+move=> x y Rx Ry; rewrite /= raddfD /= (Creal_ReP x Rx).
+by rewrite ReMr // Re_i mul0r addr0.
+Qed.
+
+Lemma Im_rect : {in real &, forall x y, 'Im (x + 'i * y) = y}.
+Proof.
+move=> x y Rx Ry; rewrite /= raddfD /= (Creal_ImP x Rx) add0r.
+by rewrite ImMr // Im_i mul1r.
+Qed.
+
+Lemma conjC_rect : {in real &, forall x y, (x + 'i * y)^* = x - 'i * y}.
+Proof.
+by move=> x y Rx Ry; rewrite /= rmorphD rmorphM conjCi mulNr !conj_Creal.
+Qed.
+
+Lemma addC_rect x1 y1 x2 y2 :
+  (x1 + 'i * y1) + (x2 + 'i * y2) = x1 + x2 + 'i * (y1 + y2).
+Proof. by rewrite addrACA -mulrDr. Qed.
+
+Lemma oppC_rect x y : - (x + 'i * y)  = - x + 'i * (- y).
+Proof. by rewrite mulrN -opprD. Qed.
+
+Lemma subC_rect x1 y1 x2 y2 :
+  (x1 + 'i * y1) - (x2 + 'i * y2) = x1 - x2 + 'i * (y1 - y2).
+Proof. by rewrite oppC_rect addC_rect. Qed.
+
+Lemma mulC_rect x1 y1 x2 y2 :
+  (x1 + 'i * y1) * (x2 + 'i * y2)
+      = x1 * x2 - y1 * y2 + 'i * (x1 * y2 + x2 * y1).
+Proof.
+rewrite mulrDl !mulrDr mulrCA -!addrA mulrAC -mulrA; congr (_ + _).
+by rewrite mulrACA -expr2 sqrCi mulN1r addrA addrC.
+Qed.
+
+Lemma normC2_rect :
+  {in real &, forall x y, `|x + 'i * y| ^+ 2 = x ^+ 2 + y ^+ 2}.
+Proof.
+move=> x y Rx Ry; rewrite /= normCK rmorphD rmorphM conjCi !conj_Creal //.
+by rewrite mulrC mulNr -subr_sqr exprMn sqrCi mulN1r opprK.
+Qed.
+
+Lemma normC2_Re_Im z : `|z| ^+ 2 = 'Re z ^+ 2 + 'Im z ^+ 2.
+Proof. by rewrite -normC2_rect -?Crect. Qed.
+
+Lemma invC_rect :
+  {in real &, forall x y, (x + 'i * y)^-1  = (x - 'i * y) / (x ^+ 2 + y ^+ 2)}.
+Proof.
+by move=> x y Rx Ry; rewrite /= invC_norm conjC_rect // mulrC normC2_rect.
+Qed.
+
+Lemma lerif_normC_Re_Creal z : `|'Re z| <= `|z| ?= iff (z \is real).
+Proof.
+rewrite -(mono_in_lerif ler_sqr); try by rewrite qualifE normr_ge0.
+rewrite normCK conj_Creal // normC2_Re_Im -expr2.
+rewrite addrC -lerif_subLR subrr (sameP (Creal_ImP _) eqP) -sqrf_eq0 eq_sym.
+by apply: lerif_eq; rewrite -realEsqr.
+Qed.
+
+Lemma lerif_Re_Creal z : 'Re z <= `|z| ?= iff (0 <= z).
+Proof.
+have ubRe: 'Re z <= `|'Re z| ?= iff (0 <= 'Re z).
+  by rewrite ger0_def eq_sym; apply/lerif_eq/real_ler_norm.
+congr (_ <= _ ?= iff _): (lerif_trans ubRe (lerif_normC_Re_Creal z)).
+apply/andP/idP=> [[zRge0 /Creal_ReP <- //] | z_ge0].
+by have Rz := ger0_real z_ge0; rewrite (Creal_ReP _ _).
+Qed.
+
+(* Equality from polar coordinates, for the upper plane. *)
+Lemma eqC_semipolar x y :
+  `|x| = `|y| -> 'Re x = 'Re y -> 0 <= 'Im x * 'Im y -> x = y.
+Proof.
+move=> eq_norm eq_Re sign_Im.
+rewrite [x]Crect [y]Crect eq_Re; congr (_ + 'i * _).
+have /eqP := congr1 (fun z => z ^+ 2) eq_norm.
+rewrite !normC2_Re_Im eq_Re (can_eq (addKr _)) eqf_sqr => /pred2P[] // eq_Im.
+rewrite eq_Im mulNr -expr2 oppr_ge0 real_exprn_even_le0 //= in sign_Im.
+by rewrite eq_Im (eqP sign_Im) oppr0.
+Qed.
+
+(* Nth roots. *)
+
+Let argCleP y z :
+  reflect (0 <= 'Im z -> 0 <= 'Im y /\ 'Re z <= 'Re y) (argCle y z).
+Proof.
+suffices dIm x: nnegIm x = (0 <= 'Im x).
+  rewrite /argCle !dIm ler_pmul2r ?invr_gt0 ?ltr0n //.
+  by apply: (iffP implyP) => geZyz /geZyz/andP.
+by rewrite /('Im x) pmulr_lge0 ?invr_gt0 ?ltr0n //; congr (0 <= _ * _).
+Qed.
+(* case Du: sqrCi => [u u2N1] /=. *)
+(* have/eqP := u2N1; rewrite -sqrCi eqf_sqr => /pred2P[] //. *)
+(* have:= conjCi; rewrite /'i; case_rootC => /= v v2n1 min_v conj_v Duv. *)
+(* have{min_v} /idPn[] := min_v u isT u2N1; rewrite negb_imply /nnegIm Du /= Duv. *)
+(* rewrite rmorphN conj_v opprK -opprD mulrNN mulNr -mulr2n mulrnAr -expr2 v2n1. *)
+(* by rewrite mulNrn opprK ler0n oppr_ge0 (ler_nat _ 2 0). *)
+
+
+Lemma rootC_Re_max n x y :
+  (n > 0)%N -> y ^+ n = x -> 0 <= 'Im y -> 'Re y <= 'Re (n.-root x).
+Proof.
+by move=> n_gt0 yn_x leI0y; case_rootC=> z /= _ /(_ y n_gt0 yn_x)/argCleP[].
+Qed.
+
+Let neg_unity_root n : (n > 1)%N -> exists2 w : C, w ^+ n = 1 & 'Re w < 0.
+Proof.
+move=> n_gt1; have [|w /eqP pw_0] := closed_rootP (\poly_(i < n) (1 : C)) _.
+  by rewrite size_poly_eq ?oner_eq0 // -(subnKC n_gt1).
+rewrite horner_poly (eq_bigr _ (fun _ _ => mul1r _)) in pw_0.
+have wn1: w ^+ n = 1 by apply/eqP; rewrite -subr_eq0 subrX1 pw_0 mulr0.
+suffices /existsP[i ltRwi0]: [exists i : 'I_n, 'Re (w ^+ i) < 0].
+  by exists (w ^+ i) => //; rewrite exprAC wn1 expr1n.
+apply: contra_eqT (congr1 Re pw_0); rewrite negb_exists => /forallP geRw0.
+rewrite raddf_sum raddf0 /= (bigD1 (Ordinal (ltnW n_gt1))) //=.
+rewrite (Creal_ReP _ _) ?rpred1 // gtr_eqF ?ltr_paddr ?ltr01 //=.
+by apply: sumr_ge0 => i _; rewrite real_lerNgt ?rpred0.
+Qed.
+
+Lemma Im_rootC_ge0 n x : (n > 1)%N -> 0 <= 'Im (n.-root x).
+Proof.
+set y := n.-root x => n_gt1; have n_gt0 := ltnW n_gt1.
+apply: wlog_neg; rewrite -real_ltrNge ?rpred0 // => ltIy0.
+suffices [z zn_x leI0z]: exists2 z, z ^+ n = x & 'Im z >= 0.
+  by rewrite /y; case_rootC => /= y1 _ /(_ z n_gt0 zn_x)/argCleP[].
+have [w wn1 ltRw0] := neg_unity_root n_gt1.
+wlog leRI0yw: w wn1 ltRw0 / 0 <= 'Re y * 'Im w.
+  move=> IHw; have: 'Re y * 'Im w \is real by rewrite rpredM.
+  case/real_ger0P=> [|/ltrW leRIyw0]; first exact: IHw.
+  apply: (IHw w^*); rewrite ?Re_conj ?Im_conj ?mulrN ?oppr_ge0 //.
+  by rewrite -rmorphX wn1 rmorph1.
+exists (w * y); first by rewrite exprMn wn1 mul1r rootCK.
+rewrite [w]Crect [y]Crect mulC_rect.
+by rewrite Im_rect ?rpredD ?rpredN 1?rpredM // addr_ge0 // ltrW ?nmulr_rgt0.
+Qed.
+
+Lemma rootC_lt0 n x : (1 < n)%N -> (n.-root x < 0) = false.
+Proof.
+set y := n.-root x => n_gt1; have n_gt0 := ltnW n_gt1.
+apply: negbTE; apply: wlog_neg => /negbNE lt0y; rewrite ler_gtF //.
+have Rx: x \is real by rewrite -[x](rootCK n_gt0) rpredX // ltr0_real.
+have Re_y: 'Re y = y by apply/Creal_ReP; rewrite ltr0_real.
+have [z zn_x leR0z]: exists2 z, z ^+ n = x & 'Re z >= 0.
+  have [w wn1 ltRw0] := neg_unity_root n_gt1.
+  exists (w * y); first by rewrite exprMn wn1 mul1r rootCK.
+  by rewrite ReMr ?ltr0_real // ltrW // nmulr_lgt0.
+without loss leI0z: z zn_x leR0z / 'Im z >= 0.
+  move=> IHz; have: 'Im z \is real by [].
+  case/real_ger0P=> [|/ltrW leIz0]; first exact: IHz.
+  apply: (IHz z^*); rewrite ?Re_conj ?Im_conj ?oppr_ge0 //.
+  by rewrite -rmorphX zn_x conj_Creal.
+by apply: ler_trans leR0z _; rewrite -Re_y ?rootC_Re_max ?ltr0_real.
+Qed.
+
+Lemma rootC_ge0 n x : (n > 0)%N -> (0 <= n.-root x) = (0 <= x).
+Proof.
+set y := n.-root x => n_gt0.
+apply/idP/idP=> [/(exprn_ge0 n) | x_ge0]; first by rewrite rootCK.
+rewrite -(ger_lerif (lerif_Re_Creal y)).
+have Ray: `|y| \is real by apply: normr_real.
+rewrite -(Creal_ReP _ Ray) rootC_Re_max ?(Creal_ImP _ Ray) //.
+by rewrite -normrX rootCK // ger0_norm.
+Qed.
+
+Lemma rootC_gt0 n x : (n > 0)%N -> (n.-root x > 0) = (x > 0).
+Proof. by move=> n_gt0; rewrite !lt0r rootC_ge0 ?rootC_eq0. Qed.
+
+Lemma rootC_le0 n x : (1 < n)%N -> (n.-root x <= 0) = (x == 0).
+Proof.
+by move=> n_gt1; rewrite ler_eqVlt rootC_lt0 // orbF rootC_eq0 1?ltnW.
+Qed.
+
+Lemma ler_rootCl n : (n > 0)%N -> {in Num.nneg, {mono n.-root : x y / x <= y}}.
+Proof.
+move=> n_gt0 x x_ge0 y; have [y_ge0 | not_y_ge0] := boolP (0 <= y).
+  by rewrite -(ler_pexpn2r n_gt0) ?qualifE ?rootC_ge0 ?rootCK.
+rewrite (contraNF (@ler_trans _ _ 0 _ _)) ?rootC_ge0 //.
+by rewrite (contraNF (ler_trans x_ge0)).
+Qed.
+
+Lemma ler_rootC n : (n > 0)%N -> {in Num.nneg &, {mono n.-root : x y / x <= y}}.
+Proof. by move=> n_gt0 x y x_ge0 _; apply: ler_rootCl. Qed.
+
+Lemma ltr_rootCl n : (n > 0)%N -> {in Num.nneg, {mono n.-root : x y / x < y}}.
+Proof. by move=> n_gt0 x x_ge0 y; rewrite !ltr_def ler_rootCl ?eqr_rootC. Qed.
+
+Lemma ltr_rootC n : (n > 0)%N -> {in Num.nneg &, {mono n.-root : x y / x < y}}.
+Proof. by move/ler_rootC/lerW_mono_in. Qed.
+
+Lemma exprCK n x : (0 < n)%N -> 0 <= x -> n.-root (x ^+ n) = x.
+Proof.
+move=> n_gt0 x_ge0; apply/eqP.
+by rewrite -(eqr_expn2 n_gt0) ?rootC_ge0 ?exprn_ge0 ?rootCK.
+Qed.
+
+Lemma norm_rootC n x : `|n.-root x| = n.-root `|x|.
+Proof.
+have [-> | n_gt0] := posnP n; first by rewrite !root0C normr0.
+apply/eqP; rewrite -(eqr_expn2 n_gt0) ?rootC_ge0 ?normr_ge0 //.
+by rewrite -normrX !rootCK.
+Qed.
+
+Lemma rootCX n x k : (n > 0)%N -> 0 <= x -> n.-root (x ^+ k) = n.-root x ^+ k.
+Proof.
+move=> n_gt0 x_ge0; apply/eqP.
+by rewrite -(eqr_expn2 n_gt0) ?(exprn_ge0, rootC_ge0) // 1?exprAC !rootCK.
+Qed.
+
+Lemma rootC1 n : (n > 0)%N -> n.-root 1 = 1.
+Proof. by move/(rootCX 0)/(_ ler01). Qed.
+
+Lemma rootCpX n x k : (k > 0)%N -> 0 <= x -> n.-root (x ^+ k) = n.-root x ^+ k.
+Proof.
+by case: n => [|n] k_gt0; [rewrite !root0C expr0n gtn_eqF | apply: rootCX].
+Qed.
+
+Lemma rootCV n x : (n > 0)%N -> 0 <= x -> n.-root x^-1 = (n.-root x)^-1.
+Proof.
+move=> n_gt0 x_ge0; apply/eqP.
+by rewrite -(eqr_expn2 n_gt0) ?(invr_ge0, rootC_ge0) // !exprVn !rootCK.
+Qed.
+
+Lemma rootC_eq1 n x : (n > 0)%N -> (n.-root x == 1) = (x == 1).
+Proof. by move=> n_gt0; rewrite -{1}(rootC1 n_gt0) eqr_rootC. Qed.
+
+Lemma rootC_ge1 n x : (n > 0)%N -> (n.-root x >= 1) = (x >= 1).
+Proof.
+by move=> n_gt0; rewrite -{1}(rootC1 n_gt0) ler_rootCl // qualifE ler01.
+Qed.
+
+Lemma rootC_gt1 n x : (n > 0)%N -> (n.-root x > 1) = (x > 1).
+Proof. by move=> n_gt0; rewrite !ltr_def rootC_eq1 ?rootC_ge1. Qed.
+
+Lemma rootC_le1 n x : (n > 0)%N -> 0 <= x -> (n.-root x <= 1) = (x <= 1).
+Proof. by move=> n_gt0 x_ge0; rewrite -{1}(rootC1 n_gt0) ler_rootCl. Qed.
+
+Lemma rootC_lt1 n x : (n > 0)%N -> 0 <= x -> (n.-root x < 1) = (x < 1).
+Proof. by move=> n_gt0 x_ge0; rewrite !ltr_neqAle rootC_eq1 ?rootC_le1. Qed.
+
+Lemma rootCMl n x z : 0 <= x -> n.-root (x * z) = n.-root x * n.-root z.
+Proof.
+rewrite le0r => /predU1P[-> | x_gt0]; first by rewrite !(mul0r, rootC0).
+have [| n_gt1 | ->] := ltngtP n 1; last by rewrite !root1C.
+  by case: n => //; rewrite !root0C mul0r.
+have [x_ge0 n_gt0] := (ltrW x_gt0, ltnW n_gt1).
+have nx_gt0: 0 < n.-root x by rewrite rootC_gt0.
+have Rnx: n.-root x \is real by rewrite ger0_real ?ltrW.
+apply: eqC_semipolar; last 1 first; try apply/eqP.
+- by rewrite ImMl // !(Im_rootC_ge0, mulr_ge0, rootC_ge0).
+- by rewrite -(eqr_expn2 n_gt0) ?normr_ge0 // -!normrX exprMn !rootCK.
+rewrite eqr_le; apply/andP; split; last first.
+  rewrite rootC_Re_max ?exprMn ?rootCK ?ImMl //.
+  by rewrite mulr_ge0 ?Im_rootC_ge0 ?ltrW.
+rewrite -[n.-root _](mulVKf (negbT (gtr_eqF nx_gt0))) !(ReMl Rnx) //.
+rewrite ler_pmul2l // rootC_Re_max ?exprMn ?exprVn ?rootCK ?mulKf ?gtr_eqF //.
+by rewrite ImMl ?rpredV // mulr_ge0 ?invr_ge0 ?Im_rootC_ge0 ?ltrW.
+Qed.
+
+Lemma rootCMr n x z : 0 <= x -> n.-root (z * x) = n.-root z * n.-root x.
+Proof. by move=> x_ge0; rewrite mulrC rootCMl // mulrC. Qed.
+
+Lemma imaginaryCE : 'i = sqrtC (-1).
+Proof.
+have : sqrtC (-1) ^+ 2 - 'i ^+ 2 == 0 by rewrite sqrCi rootCK // subrr.
+rewrite subr_sqr mulf_eq0 subr_eq0 addr_eq0; have [//|_/= /eqP sCN1E] := eqP.
+by have := @Im_rootC_ge0 2 (-1) isT; rewrite sCN1E raddfN /= Im_i ler0N1.
+Qed.
+
+(* More properties of n.-root will be established in cyclotomic.v. *)
+
+(* The proper form of the Arithmetic - Geometric Mean inequality. *)
+
+Lemma lerif_rootC_AGM (I : finType) (A : pred I) (n := #|A|) E :
+    {in A, forall i, 0 <= E i} ->
+  n.-root (\prod_(i in A) E i) <= (\sum_(i in A) E i) / n%:R
+                             ?= iff [forall i in A, forall j in A, E i == E j].
+Proof.
+move=> Ege0; have [n0 | n_gt0] := posnP n.
+  rewrite n0 root0C invr0 mulr0; apply/lerif_refl/forall_inP=> i.
+  by rewrite (card0_eq n0).
+rewrite -(mono_in_lerif (ler_pexpn2r n_gt0)) ?rootCK //=; first 1 last.
+- by rewrite qualifE rootC_ge0 // prodr_ge0.
+- by rewrite rpred_div ?rpred_nat ?rpred_sum.
+exact: lerif_AGM.
+Qed.
+
+(* Square root. *)
+
+Lemma sqrtC0 : sqrtC 0 = 0. Proof. exact: rootC0. Qed.
+Lemma sqrtC1 : sqrtC 1 = 1. Proof. exact: rootC1. Qed.
+Lemma sqrtCK x : sqrtC x ^+ 2 = x. Proof. exact: rootCK. Qed.
+Lemma sqrCK x : 0 <= x -> sqrtC (x ^+ 2) = x. Proof. exact: exprCK. Qed.
+
+Lemma sqrtC_ge0 x : (0 <= sqrtC x) = (0 <= x). Proof. exact: rootC_ge0. Qed.
+Lemma sqrtC_eq0 x : (sqrtC x == 0) = (x == 0). Proof. exact: rootC_eq0. Qed.
+Lemma sqrtC_gt0 x : (sqrtC x > 0) = (x > 0). Proof. exact: rootC_gt0. Qed.
+Lemma sqrtC_lt0 x : (sqrtC x < 0) = false. Proof. exact: rootC_lt0. Qed.
+Lemma sqrtC_le0 x : (sqrtC x <= 0) = (x == 0). Proof. exact: rootC_le0. Qed.
+
+Lemma ler_sqrtC : {in Num.nneg &, {mono sqrtC : x y / x <= y}}.
+Proof. exact: ler_rootC. Qed.
+Lemma ltr_sqrtC : {in Num.nneg &, {mono sqrtC : x y / x < y}}.
+Proof. exact: ltr_rootC. Qed.
+Lemma eqr_sqrtC : {mono sqrtC : x y / x == y}.
+Proof. exact: eqr_rootC. Qed.
+Lemma sqrtC_inj : injective sqrtC.
+Proof. exact: rootC_inj. Qed.
+Lemma sqrtCM : {in Num.nneg &, {morph sqrtC : x y / x * y}}.
+Proof. by move=> x y _; apply: rootCMr. Qed.
+
+Lemma sqrCK_P x : reflect (sqrtC (x ^+ 2) = x) ((0 <= 'Im x) && ~~ (x < 0)).
+Proof.
+apply: (iffP andP) => [[leI0x not_gt0x] | <-]; last first.
+  by rewrite sqrtC_lt0 Im_rootC_ge0.
+have /eqP := sqrtCK (x ^+ 2); rewrite eqf_sqr => /pred2P[] // defNx.
+apply: sqrCK; rewrite -real_lerNgt ?rpred0 // in not_gt0x;
+apply/Creal_ImP/ler_anti;
+by rewrite leI0x -oppr_ge0 -raddfN -defNx Im_rootC_ge0.
+Qed.
+
+Lemma normC_def x : `|x| = sqrtC (x * x^*).
+Proof. by rewrite -normCK sqrCK ?normr_ge0. Qed.
+
+Lemma norm_conjC x : `|x^*| = `|x|.
+Proof. by rewrite !normC_def conjCK mulrC. Qed.
+
+Lemma normC_rect :
+  {in real &, forall x y, `|x + 'i * y| = sqrtC (x ^+ 2 + y ^+ 2)}.
+Proof. by move=> x y Rx Ry; rewrite /= normC_def -normCK normC2_rect. Qed.
+
+Lemma normC_Re_Im z : `|z| = sqrtC ('Re z ^+ 2 + 'Im z ^+ 2).
+Proof. by rewrite normC_def -normCK normC2_Re_Im. Qed.
+
+(* Norm sum (in)equalities. *)
+
+Lemma normC_add_eq x y :
+    `|x + y| = `|x| + `|y| ->
+  {t : C | `|t| == 1 & (x, y) = (`|x| * t, `|y| * t)}.
+Proof.
+move=> lin_xy; apply: sig2_eqW; pose u z := if z == 0 then 1 else z / `|z|.
+have uE z: (`|u z| = 1) * (`|z| * u z = z).
+  rewrite /u; have [->|nz_z] := altP eqP; first by rewrite normr0 normr1 mul0r.
+  by rewrite normf_div normr_id mulrCA divff ?mulr1 ?normr_eq0.
+have [->|nz_x] := eqVneq x 0; first by exists (u y); rewrite uE ?normr0 ?mul0r.
+exists (u x); rewrite uE // /u (negPf nz_x); congr (_ , _).
+have{lin_xy} def2xy: `|x| * `|y| *+ 2 = x * y ^* + y * x ^*.
+  apply/(addrI (x * x^*))/(addIr (y * y^*)); rewrite -2!{1}normCK -sqrrD.
+  by rewrite addrA -addrA -!mulrDr -mulrDl -rmorphD -normCK lin_xy.
+have def_xy: x * y^* = y * x^*.
+  apply/eqP; rewrite -subr_eq0 -[_ == 0](@expf_eq0 _ _ 2).
+  rewrite (canRL (subrK _) (subr_sqrDB _ _)) opprK -def2xy exprMn_n exprMn.
+  by rewrite mulrN mulrAC mulrA -mulrA mulrACA -!normCK mulNrn addNr.
+have{def_xy def2xy} def_yx: `|y * x| = y * x^*.
+  by apply: (mulIf nz2); rewrite !mulr_natr mulrC normrM def2xy def_xy.
+rewrite -{1}(divfK nz_x y) invC_norm mulrCA -{}def_yx !normrM invfM.
+by rewrite mulrCA divfK ?normr_eq0 // mulrAC mulrA.
+Qed.
+
+Lemma normC_sum_eq (I : finType) (P : pred I) (F : I -> C) :
+     `|\sum_(i | P i) F i| = \sum_(i | P i) `|F i| ->
+   {t : C | `|t| == 1 & forall i, P i -> F i = `|F i| * t}.
+Proof.
+have [i /andP[Pi nzFi] | F0] := pickP [pred i | P i & F i != 0]; last first.
+  exists 1 => [|i Pi]; first by rewrite normr1.
+  by case/nandP: (F0 i) => [/negP[]// | /negbNE/eqP->]; rewrite normr0 mul0r.
+rewrite !(bigD1 i Pi) /= => norm_sumF; pose Q j := P j && (j != i).
+rewrite -normr_eq0 in nzFi; set c := F i / `|F i|; exists c => [|j Pj].
+  by rewrite normrM normfV normr_id divff.
+have [Qj | /nandP[/negP[]// | /negbNE/eqP->]] := boolP (Q j); last first.
+  by rewrite mulrC divfK.
+have: `|F i + F j| = `|F i| + `|F j|.
+  do [rewrite !(bigD1 j Qj) /=; set z := \sum_(k | _) `|_|] in norm_sumF.
+  apply/eqP; rewrite eqr_le ler_norm_add -(ler_add2r z) -addrA -norm_sumF addrA.
+  by rewrite (ler_trans (ler_norm_add _ _)) // ler_add2l ler_norm_sum.
+by case/normC_add_eq=> k _ [/(canLR (mulKf nzFi)) <-]; rewrite -(mulrC (F i)).
+Qed.
+
+Lemma normC_sum_eq1 (I : finType) (P : pred I) (F : I -> C) :
+    `|\sum_(i | P i) F i| = (\sum_(i | P i) `|F i|) ->
+     (forall i, P i -> `|F i| = 1) ->
+   {t : C | `|t| == 1 & forall i, P i -> F i = t}.
+Proof.
+case/normC_sum_eq=> t t1 defF normF.
+by exists t => // i Pi; rewrite defF // normF // mul1r.
+Qed.
+
+Lemma normC_sum_upper (I : finType) (P : pred I) (F G : I -> C) :
+     (forall i, P i -> `|F i| <= G i) ->
+     \sum_(i | P i) F i = \sum_(i | P i) G i ->
+   forall i, P i -> F i = G i.
+Proof.
+set sumF := \sum_(i | _) _; set sumG := \sum_(i | _) _ => leFG eq_sumFG.
+have posG i: P i -> 0 <= G i by move/leFG; apply: ler_trans; apply: normr_ge0.
+have norm_sumG: `|sumG| = sumG by rewrite ger0_norm ?sumr_ge0.
+have norm_sumF: `|sumF| = \sum_(i | P i) `|F i|.
+  apply/eqP; rewrite eqr_le ler_norm_sum eq_sumFG norm_sumG -subr_ge0 -sumrB.
+  by rewrite sumr_ge0 // => i Pi; rewrite subr_ge0 ?leFG.
+have [t _ defF] := normC_sum_eq norm_sumF.
+have [/(psumr_eq0P posG) G0 i Pi | nz_sumG] := eqVneq sumG 0.
+  by apply/eqP; rewrite G0 // -normr_eq0 eqr_le normr_ge0 -(G0 i Pi) leFG.
+have t1: t = 1.
+  apply: (mulfI nz_sumG); rewrite mulr1 -{1}norm_sumG -eq_sumFG norm_sumF.
+  by rewrite mulr_suml -(eq_bigr _ defF).
+have /psumr_eq0P eqFG i: P i -> 0 <= G i - F i.
+  by move=> Pi; rewrite subr_ge0 defF // t1 mulr1 leFG.
+move=> i /eqFG/(canRL (subrK _))->; rewrite ?add0r //.
+by rewrite sumrB -/sumF eq_sumFG subrr.
+Qed.
+
+Lemma normC_sub_eq x y :
+  `|x - y| = `|x| - `|y| -> {t | `|t| == 1 & (x, y) = (`|x| * t, `|y| * t)}.
+Proof.
+rewrite -{-1}(subrK y x) => /(canLR (subrK _))/esym-Dx; rewrite Dx.
+by have [t ? [Dxy Dy]] := normC_add_eq Dx; exists t; rewrite // mulrDl -Dxy -Dy.
+Qed.
+
+End ClosedFieldTheory.
+
+Notation "n .-root" := (@nthroot _ n) (at level 2, format "n .-root") : ring_scope.
+Notation sqrtC := 2.-root.
+Notation "'i" := (@imaginaryC _) (at level 0) : ring_scope.
+Notation "'Re z" := (Re z) (at level 10, z at level 8) : ring_scope.
+Notation "'Im z" := (Im z) (at level 10, z at level 8) : ring_scope.
+
 End Theory.
 
 Module RealMixin.
@@ -4225,3 +4936,4 @@ Export Num.Syntax Num.PredInstances.
 Notation RealLeMixin := Num.RealMixin.Le.
 Notation RealLtMixin := Num.RealMixin.Lt.
 Notation RealLeAxiom R := (Num.RealMixin.Real (Phant R) (erefl _)).
+Notation ImaginaryMixin := Num.ClosedField.ImaginaryMixin.
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v
index e1d721e..da6dc59 100644
--- a/mathcomp/algebra/vector.v
+++ b/mathcomp/algebra/vector.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v
index 543b9e5..ec9750a 100644
--- a/mathcomp/algebra/zmodp.v
+++ b/mathcomp/algebra/zmodp.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp