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

34 files changed, 51 insertions, 50 deletions

diff --git a/mathcomp/odd_order/BGappendixAB.v b/mathcomp/odd_order/BGappendixAB.v
index f1ec1b2..cb104f4 100644
--- a/mathcomp/odd_order/BGappendixAB.v
+++ b/mathcomp/odd_order/BGappendixAB.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/odd_order/BGappendixC.v b/mathcomp/odd_order/BGappendixC.v
index a64c49a..f8b9137 100644
--- a/mathcomp/odd_order/BGappendixC.v
+++ b/mathcomp/odd_order/BGappendixC.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
@@ -288,7 +288,7 @@ Proof.
 have [q_gt4 | q_le4] := ltnP 4 q.
   pose inK x := enum_rank_in (classes1 H) (x ^: H).
   have inK_E x: x \in H -> enum_val (inK x) = x ^: H.
-    by move=> Hx; rewrite enum_rankK_in ?mem_classes. 
+    by move=> Hx; rewrite enum_rankK_in ?mem_classes.
   pose j := inK s; pose k := inK (s ^+ 2)%g; pose e := gring_classM_coef j j k.
   have cPP: abelian P by rewrite -(injm_abelian inj_sigma) ?zmod_abelian.
   have Hs: s \in H by rewrite -(sdprodW defH) -[s]mulg1 mem_mulg.
@@ -355,18 +355,19 @@ have [q_gt4 | q_le4] := ltnP 4 q.
       by rewrite sub_cent1 groupX // (subsetP cPP).
     rewrite mulrnA -second_orthogonality_relation ?groupX // big_mkcond.
     by apply: ler_sum => i _; rewrite normCK; case: ifP; rewrite ?mul_conjC_ge0.
-  have sqrtP_gt0: 0 < sqrtC #|P|%:R by rewrite sqrtC_gt0 ?gt0CG.
-  have{De ub_linH'}: `|(#|P| * e)%:R - #|U|%:R ^+ 2| <= #|P|%:R * sqrtC #|P|%:R.
+  have sqrtP_gt0: 0 < sqrtC #|P|%:R :> algC by rewrite sqrtC_gt0 ?gt0CG.
+  have{De ub_linH'}:
+    `|(#|P| * e)%:R - #|U|%:R ^+ 2| <= #|P|%:R * sqrtC #|P|%:R :> algC.
     rewrite natrM De mulrCA mulrA divfK ?neq0CG // (bigID linH) /= sum_linH.
     rewrite mulrDr addrC addKr mulrC mulr_suml /chi_s2.
     rewrite (ler_trans (ler_norm_sum _ _ _)) // -ler_pdivr_mulr // mulr_suml.
     apply: ler_trans (ub_linH' 1%N isT); apply: ler_sum => i linH'i.
     rewrite ler_pdivr_mulr // degU ?divfK ?neq0CG //.
     rewrite normrM -normrX norm_conjC ler_wpmul2l ?normr_ge0 //.
-    rewrite -ler_sqr ?qualifE ?normr_ge0 ?(@ltrW _ 0) // sqrtCK. 
+    rewrite -ler_sqr ?qualifE ?normr_ge0 ?(@ltrW _ 0) // sqrtCK.
     apply: ler_trans (ub_linH' 2 isT); rewrite (bigD1 i) ?ler_paddr //=.
     by apply: sumr_ge0 => i1 _; rewrite exprn_ge0 ?normr_ge0.
-  rewrite natrM real_ler_distl ?rpredB ?rpredM ?rpred_nat // => /andP[lb_Pe _]. 
+  rewrite natrM real_ler_distl ?rpredB ?rpredM ?rpred_nat // => /andP[lb_Pe _].
   rewrite -ltC_nat -(ltr_pmul2l (gt0CG P)) {lb_Pe}(ltr_le_trans _ lb_Pe) //.
   rewrite ltr_subr_addl (@ler_lt_trans _ ((p ^ q.-1)%:R ^+ 2)) //; last first.
     rewrite  -!natrX ltC_nat ltn_sqr oU ltn_divRL ?dvdn_pred_predX //.
diff --git a/mathcomp/odd_order/BGsection1.v b/mathcomp/odd_order/BGsection1.v
index 79bb387..7539af3 100644
--- a/mathcomp/odd_order/BGsection1.v
+++ b/mathcomp/odd_order/BGsection1.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/odd_order/BGsection10.v b/mathcomp/odd_order/BGsection10.v
index 6c8e91b..5a61e25 100644
--- a/mathcomp/odd_order/BGsection10.v
+++ b/mathcomp/odd_order/BGsection10.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/odd_order/BGsection11.v b/mathcomp/odd_order/BGsection11.v
index fa3cd65..fe41e8d 100644
--- a/mathcomp/odd_order/BGsection11.v
+++ b/mathcomp/odd_order/BGsection11.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/odd_order/BGsection12.v b/mathcomp/odd_order/BGsection12.v
index a266ed3..1dc8454 100644
--- a/mathcomp/odd_order/BGsection12.v
+++ b/mathcomp/odd_order/BGsection12.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/odd_order/BGsection13.v b/mathcomp/odd_order/BGsection13.v
index 13b7dcb..e90be7f 100644
--- a/mathcomp/odd_order/BGsection13.v
+++ b/mathcomp/odd_order/BGsection13.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/odd_order/BGsection14.v b/mathcomp/odd_order/BGsection14.v
index 18d4b08..2e3f523 100644
--- a/mathcomp/odd_order/BGsection14.v
+++ b/mathcomp/odd_order/BGsection14.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/odd_order/BGsection15.v b/mathcomp/odd_order/BGsection15.v
index 553feda..06d7eb9 100644
--- a/mathcomp/odd_order/BGsection15.v
+++ b/mathcomp/odd_order/BGsection15.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/odd_order/BGsection16.v b/mathcomp/odd_order/BGsection16.v
index 32850e4..737a92d 100644
--- a/mathcomp/odd_order/BGsection16.v
+++ b/mathcomp/odd_order/BGsection16.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/odd_order/BGsection2.v b/mathcomp/odd_order/BGsection2.v
index 9008cf8..5d7a899 100644
--- a/mathcomp/odd_order/BGsection2.v
+++ b/mathcomp/odd_order/BGsection2.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/odd_order/BGsection3.v b/mathcomp/odd_order/BGsection3.v
index 03455c3..007aaf4 100644
--- a/mathcomp/odd_order/BGsection3.v
+++ b/mathcomp/odd_order/BGsection3.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/odd_order/BGsection4.v b/mathcomp/odd_order/BGsection4.v
index a9b519a..217f151 100644
--- a/mathcomp/odd_order/BGsection4.v
+++ b/mathcomp/odd_order/BGsection4.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/odd_order/BGsection5.v b/mathcomp/odd_order/BGsection5.v
index 50f8e21..bf84a99 100644
--- a/mathcomp/odd_order/BGsection5.v
+++ b/mathcomp/odd_order/BGsection5.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/odd_order/BGsection6.v b/mathcomp/odd_order/BGsection6.v
index 6d2df4d..e344b98 100644
--- a/mathcomp/odd_order/BGsection6.v
+++ b/mathcomp/odd_order/BGsection6.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/odd_order/BGsection7.v b/mathcomp/odd_order/BGsection7.v
index 6af8f7d..71e800e 100644
--- a/mathcomp/odd_order/BGsection7.v
+++ b/mathcomp/odd_order/BGsection7.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/odd_order/BGsection8.v b/mathcomp/odd_order/BGsection8.v
index 9ced163..db378f3 100644
--- a/mathcomp/odd_order/BGsection8.v
+++ b/mathcomp/odd_order/BGsection8.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/odd_order/BGsection9.v b/mathcomp/odd_order/BGsection9.v
index 3baa270..f649e84 100644
--- a/mathcomp/odd_order/BGsection9.v
+++ b/mathcomp/odd_order/BGsection9.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/odd_order/PFsection1.v b/mathcomp/odd_order/PFsection1.v
index 7c74766..1d784ed 100644
--- a/mathcomp/odd_order/PFsection1.v
+++ b/mathcomp/odd_order/PFsection1.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/odd_order/PFsection10.v b/mathcomp/odd_order/PFsection10.v
index 18fbf8c..11b3b20 100644
--- a/mathcomp/odd_order/PFsection10.v
+++ b/mathcomp/odd_order/PFsection10.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/odd_order/PFsection11.v b/mathcomp/odd_order/PFsection11.v
index b966f25..c37633f 100644
--- a/mathcomp/odd_order/PFsection11.v
+++ b/mathcomp/odd_order/PFsection11.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
@@ -232,7 +232,7 @@ Lemma bounded_proper_coherent H1 :
     (#|HU : H1| <= 2 * q * #|U : C| + 1)%N.
 Proof.
 move=> nsH1_M psH1_M' cohH1; have [nsHHU _ _ _ _] := sdprod_context defHU.
-suffices: #|HU : H1|%:R - 1 <= 2%:R * #|M : HC|%:R * sqrtC #|HC : HC|%:R.
+suffices: #|HU : H1|%:R - 1 <= 2%:R * #|M : HC|%:R * sqrtC #|HC : HC|%:R :> algC.
   rewrite  indexgg sqrtC1 mulr1 -leC_nat natrD -ler_subl_addr -mulnA natrM.
   congr (_ <= _ * _%:R); apply/eqP; rewrite -(eqn_pmul2l (cardG_gt0 HC)).
   rewrite Lagrange ?normal_sub // mulnCA -(dprod_card defHC) -mulnA mulnC.
diff --git a/mathcomp/odd_order/PFsection12.v b/mathcomp/odd_order/PFsection12.v
index fa5a453..fcc35bf 100644
--- a/mathcomp/odd_order/PFsection12.v
+++ b/mathcomp/odd_order/PFsection12.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/odd_order/PFsection13.v b/mathcomp/odd_order/PFsection13.v
index 1ab2aee..18e8606 100644
--- a/mathcomp/odd_order/PFsection13.v
+++ b/mathcomp/odd_order/PFsection13.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/odd_order/PFsection14.v b/mathcomp/odd_order/PFsection14.v
index 5c43caa..c634ec1 100644
--- a/mathcomp/odd_order/PFsection14.v
+++ b/mathcomp/odd_order/PFsection14.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/odd_order/PFsection2.v b/mathcomp/odd_order/PFsection2.v
index 04c4eba..f92bb16 100644
--- a/mathcomp/odd_order/PFsection2.v
+++ b/mathcomp/odd_order/PFsection2.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/odd_order/PFsection3.v b/mathcomp/odd_order/PFsection3.v
index cb55ae4..eb5ccf8 100644
--- a/mathcomp/odd_order/PFsection3.v
+++ b/mathcomp/odd_order/PFsection3.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
@@ -1360,7 +1360,7 @@ have{oxi_00} oxi_i0 i j i0: '[xi_ i j, xi_ i0 0] = ((i == i0) && (j == 0))%:R.
   by rewrite cfdotC Xi0_X0j // conjC0.
 have [-> | nzi2] := altP (i2 =P 0); first exact: oxi_0j.
 have [-> | nzj2] := altP (j2 =P 0); first exact: oxi_i0.
-rewrite cfdotC eq_sym; apply: canLR conjCK _; rewrite rmorph_nat.
+rewrite cfdotC eq_sym; apply: canLR (@conjCK _) _; rewrite rmorph_nat.
 have [-> | nzi1] := altP (i1 =P 0); first exact: oxi_0j.
 have [-> | nzj1] := altP (j1 =P 0); first exact: oxi_i0.
 have ->: xi_ i1 j1 = beta i1 j1 + xi_ i1 0 + xi_ 0 j1 by rewrite /xi_ !ifN.
diff --git a/mathcomp/odd_order/PFsection4.v b/mathcomp/odd_order/PFsection4.v
index 01ca8a5..c897e84 100644
--- a/mathcomp/odd_order/PFsection4.v
+++ b/mathcomp/odd_order/PFsection4.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/odd_order/PFsection5.v b/mathcomp/odd_order/PFsection5.v
index d318f5f..636c48c 100644
--- a/mathcomp/odd_order/PFsection5.v
+++ b/mathcomp/odd_order/PFsection5.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
@@ -492,7 +492,7 @@ Definition subcoherent S tau R :=
       (*c*) pairwise_orthogonal S,
       (*d*) {in S, forall xi : 'CF(L : {set gT}),
               [/\ {subset R xi <= 'Z[irr G]}, orthonormal (R xi)
-                & tau (xi - xi^*)%CF = \sum_(alpha <- R xi) alpha]}
+                & tau (xi - xi^*%CF) = \sum_(alpha <- R xi) alpha]}
     & (*e*) {in S &, forall xi phi : 'CF(L),
               orthogonal phi (xi :: xi^*%CF) -> orthogonal (R phi) (R xi)}].
 
@@ -621,7 +621,7 @@ have isoS1: {in S1, isometry [eta tau with eta1 |-> zeta1], to 'Z[irr G]}.
   split=> [xi eta | eta]; rewrite !in_cons /=; last first.
     by case: eqP => [-> | _  /isoS[/Ztau/zcharW]].
   do 2!case: eqP => [-> _|_  /isoS[? ?]] //; last exact: Itau.
-  by apply/(can_inj conjCK); rewrite -!cfdotC.
+  by apply/(can_inj (@conjCK _)); rewrite -!cfdotC.
 have [nu Dnu IZnu] := Zisometry_of_iso freeS1 isoS1.
 exists nu; split=> // phi; rewrite zcharD1E => /andP[].
 case/(zchar_expansion (free_uniq freeS1)) => b Zb {phi}-> phi1_0.
@@ -646,7 +646,7 @@ have N_S: {subset S <= character} by move=> _ /irrS/irrP[i ->]; apply: irr_char.
 have Z_S: {subset S <= 'Z[irr L]} by move=> chi /N_S/char_vchar.
 have o1S: orthonormal S by apply: sub_orthonormal (irr_orthonormal L).
 have [[_ dotSS] oS] := (orthonormalP o1S, orthonormal_orthogonal o1S).
-pose beta chi := tau (chi - chi^*)%CF; pose eqBP := _ =P beta _.
+pose beta chi := tau (chi - chi^*%CF); pose eqBP := _ =P beta _.
 have Zbeta: {in S, forall chi, chi - (chi^*)%CF \in 'Z[S, L^#]}.
   move=> chi Schi; rewrite /= zcharD1E rpredB ?mem_zchar ?ccS //= !cfunE.
   by rewrite subr_eq0 conj_Cnat // Cnat_char1 ?N_S.
@@ -885,7 +885,7 @@ Lemma subcoherent_norm chi psi (tau1 : {additive 'CF(L) -> 'CF(G)}) X Y :
     [/\ chi \in S, psi \in 'Z[irr L] & orthogonal (chi :: chi^*)%CF psi] ->
     let S0 := chi - psi :: chi - chi^*%CF in
     {in 'Z[S0], isometry tau1, to 'Z[irr G]} ->
-    tau1 (chi - chi^*)%CF = tau (chi - chi^*)%CF ->
+    tau1 (chi - chi^*%CF) = tau (chi - chi^*%CF) ->
     [/\ tau1 (chi - psi) = X - Y, '[X, Y] = 0 & orthogonal Y (R chi)] ->
  [/\ (*a*) '[chi] <= '[X]
    & (*b*) '[psi] <= '[Y] ->
diff --git a/mathcomp/odd_order/PFsection6.v b/mathcomp/odd_order/PFsection6.v
index 6d9ecfc..b32a57d 100644
--- a/mathcomp/odd_order/PFsection6.v
+++ b/mathcomp/odd_order/PFsection6.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
@@ -83,13 +83,13 @@ Lemma coherent_seqIndD_bound (A B C D : {group gT}) :
   (*a*) [/\ A \proper K, B \subset D, D \subset C, C \subset K
           & D / B \subset 'Z(C / B)]%g ->
   (*b*) coherent (S A) L^# tau -> \unless coherent (S B) L^# tau,
-  #|K : A|%:R - 1 <= 2%:R * #|L : C|%:R * sqrtC #|C : D|%:R.
+  #|K : A|%:R - 1 <= 2%:R * #|L : C|%:R * sqrtC #|C : D|%:R :> algC.
 Proof.
 move=> [nsAL nsBL nsCL nsDL] [ltAK sBD sDC sCK sDbZC] cohA.
 have sBC := subset_trans sBD sDC; have sBK := subset_trans sBC sCK.
 have [sAK nsBK] := (proper_sub ltAK, normalS sBK sKL nsBL).
 have{sBC} [nsAK nsBC] := (normalS sAK sKL nsAL, normalS sBC sCK nsBK).
-rewrite real_lerNgt ?rpredB ?ger0_real ?mulr_ge0 ?sqrtC_ge0 ?ler0n //.
+rewrite real_lerNgt ?rpredB ?ger0_real ?mulr_ge0 ?sqrtC_ge0 ?ler0n ?ler01 //.
 apply/unless_contra; rewrite negbK -(Lagrange_index sKL sCK) natrM => lb_KA.
 pose S2 : seq 'CF(L) := [::]; pose S1 := S2 ++ S A; rewrite -[S A]/S1 in cohA.
 have ccsS1S: cfConjC_subset S1 calS by apply: seqInd_conjC_subset1.
@@ -153,7 +153,7 @@ have sAbZH: (A / B \subset 'Z(H / B))%g.
   by apply: homg_quotientS; rewrite ?(subset_trans sHL) ?normal_norm.
 have ltAH: A \proper H.
   by rewrite properEneq sAH (contraTneq _ lbHA) // => ->; rewrite indexgg addn1.
-set x := sqrtC #|H : A|%:R.
+set x : algC := sqrtC #|H : A|%:R.
 have [nz_x x_gt0]: x != 0 /\ 0 < x by rewrite gtr_eqF sqrtC_gt0 gt0CiG.
 without loss{cohA} ubKA: / #|K : A|%:R - 1 <= 2%:R * #|L : H|%:R * x.
   have [sAK ltAK] := (subset_trans sAH sHK, proper_sub_trans ltAH sHK).
diff --git a/mathcomp/odd_order/PFsection7.v b/mathcomp/odd_order/PFsection7.v
index cea9319..455681c 100644
--- a/mathcomp/odd_order/PFsection7.v
+++ b/mathcomp/odd_order/PFsection7.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
@@ -324,7 +324,7 @@ transitivity (\sum_(x in A) \sum_(xi <- S) \sum_(mu <- S) F xi mu x).
   apply: eq_bigr => x Ax; rewrite part_a // sum_cfunE -mulrA mulr_suml.
   apply: eq_bigr => xi _; rewrite mulrA -mulr_suml rmorph_sum; congr (_ * _).
   rewrite mulr_sumr; apply: eq_bigr => mu _; rewrite !cfunE (cfdotC mu).
-  rewrite -{1}[mu x]conjCK -fmorph_div -rmorphM conjCK -4!mulrA 2!(mulrCA _^-1).
+  rewrite -{1}[mu x]conjCK -fmorph_div -rmorphM conjCK -3!mulrA 2!(mulrCA _^-1).
   by rewrite (mulrA _^-1) -invfM 2!(mulrCA (xi x)) mulrA 2!(mulrA _^*).
 rewrite exchange_big; apply: eq_bigr => xi _; rewrite exchange_big /=.
 apply: eq_big_seq => mu Smu; have Tmu := sST mu Smu.
diff --git a/mathcomp/odd_order/PFsection8.v b/mathcomp/odd_order/PFsection8.v
index fd085f6..d4ffa46 100644
--- a/mathcomp/odd_order/PFsection8.v
+++ b/mathcomp/odd_order/PFsection8.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/odd_order/PFsection9.v b/mathcomp/odd_order/PFsection9.v
index 63e10bb..0cd1109 100644
--- a/mathcomp/odd_order/PFsection9.v
+++ b/mathcomp/odd_order/PFsection9.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
@@ -1953,7 +1953,7 @@ have [gtS4alpha s4gt0]: (size S4)%:R > '[alpha] /\ (size S4 > 0)%N.
       rewrite ltn_pmul2r ?expn_gt0 ?a_gt0 // -doubleS.
       by rewrite -(prednK q_gt0) expnS mul2n leq_double ltn_expl.
     rewrite mulnA leq_pmul2r ?expn_gt0 ?a_gt0 // -(subnKC q_gt2).
-    rewrite mulnCA mulnA addSn -mul_Sm_binm bin1 -mulnA leq_pmul2l //.
+    rewrite mulnCA mulnA addSn -mul_bin_diag bin1 -mulnA leq_pmul2l //.
     by rewrite mulnS -addSnnS leq_addr.
   rewrite Dp -Da_p mul2n (addnC a.*2) expnDn -(subnKC q_gt2) !addSn add0n.
   rewrite 3!big_ord_recl big_ord_recr /= !exp1n /= bin1 binn !mul1n /bump /=.
diff --git a/mathcomp/odd_order/stripped_odd_order_theorem.v b/mathcomp/odd_order/stripped_odd_order_theorem.v
index 05c24a9..19b9d0b 100644
--- a/mathcomp/odd_order/stripped_odd_order_theorem.v
+++ b/mathcomp/odd_order/stripped_odd_order_theorem.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 mathcomp.ssreflect.ssreflect.
 From mathcomp
diff --git a/mathcomp/odd_order/wielandt_fixpoint.v b/mathcomp/odd_order/wielandt_fixpoint.v
index 4f40c11..3a9a099 100644
--- a/mathcomp/odd_order/wielandt_fixpoint.v
+++ b/mathcomp/odd_order/wielandt_fixpoint.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