Merge pull request #75 from math-comp/fix_conj

Adapt to math-comp/math-comp#1404

Author: proux01

theories/PFsection10.v

@@ -375,7 +375,7 @@ have cohS2 : coherent_with S2 M^# tau tau1 := subset_coherent_with sS21 cohS1.
 have irrS2: {subset S2 <= irr M} by apply/allP; rewrite /= cfAut_irr irr_zeta.
 rewrite (FTtype345_bridge_coherence cohS2 Dalpha) //; last first.
   rewrite -[X]opprK cfdotNr opprD cfdotDr nY_n2 cfdotNl cfdotNr opprK cfdotZl.
-  by rewrite cfdotC alpha_zeta_n rmorphN conj_natr // mulrN addNr oppr0.
+  by rewrite cfdotC alpha_zeta_n rmorphN/= conj_natr // mulrN addNr oppr0.
 split=> [|_ /sS21/sS10//|]; last first.
   by apply/allP; rewrite /= !inE cfConjCK !eqxx orbT.
 by rewrite /= inE eq_sym; have [[_ /hasPn-> //]] := scohS0; apply: sS10.

theories/PFsection11.v

@@ -26,7 +26,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Import GroupScope Order.TTheory GRing.Theory FinRing.Theory Num.Theory.
+Import GroupScope Order.TTheory GRing.Theory FinRing.Theory Num.Theory Num.Def.
 
 Section Eleven.
 
@@ -867,7 +867,7 @@ have tau_alpha i: tau (alpha_ i j) = eta_ i j - eta_ i 0 - n *: zeta1.
     rewrite cfdotC Dphi cfdotDl (orthoPl oXS1) ?map_f // addr0.
     rewrite defY cfdotBl scaler_sumr cfproj_sum_orthonormal //.
     rewrite cfdotZl Itau1 ?mem_zchar ?n1S1 // mulr1 rmorphB opprD opprK.
-    by rewrite Dn rmorph_nat conj_intr.
+    by rewrite Dn rmorph_nat/= conj_intr.
     have a_even: (2 %| a)%C. (* Third internal part of (11.8.5). *)
     have Zbeta: beta \in 'Z[irr G].
       rewrite -{1}(betaE i j) // rpredD ?rpredB ?Zphi ?cycTIiso_vchar //.

theories/PFsection14.v

@@ -27,7 +27,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Import GroupScope Order.TTheory GRing.Theory FinRing.Theory Num.Theory.
+Import GroupScope Order.TTheory GRing.Theory FinRing.Theory Num.Theory Num.Def.
 
 Section Fourteen.
 
@@ -1257,5 +1257,3 @@ Proof. exact: (minSimpleOdd_ind no_minSimple_odd_group). Qed.
 Theorem simple_odd_group_prime (gT : finGroupType) (G : {group gT}) :
   odd #|G| -> simple G -> prime #|G|.
 Proof. exact: (minSimpleOdd_prime no_minSimple_odd_group). Qed.
-
-

theories/PFsection5.v

@@ -49,7 +49,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Import GroupScope Order.TTheory GRing.Theory Num.Theory.
+Import GroupScope Order.TTheory GRing.Theory Num.Theory Num.Def.
 Local Open Scope ring_scope.
 
 (* Results about the set of induced irreducible characters *)

theories/PFsection9.v

@@ -38,7 +38,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Import GroupScope Order.TTheory GRing.Theory FinRing.Theory.
+Import GroupScope Order.TTheory GRing.Theory FinRing.Theory Num.Theory Num.Def.
 
 Section Nine.
 
@@ -2121,7 +2121,7 @@ have [Gamma [S4_Gamma normGamma [b Dbeta]]]:
     rewrite -raddfB Dtau1 // Itau //; last first.
       by rewrite sS0A // zchar_split rpredB ?mem_zchar ?(zchar_on Z1dpsi).
     rewrite cfdotC cfdotBr cfdotZr !cfdotBl 2?oSS ?(memPn S1'lam1) // subrr.
-    by rewrite add0r n1psi1 oSS // subr0 mulr1 rmorphN conjCK subrr scale0r.
+    by rewrite add0r n1psi1 oSS // subr0 mulr1 rmorphN/= conjCK subrr scale0r.
   have Gge1: 1 <= '[G] ?= iff ('[G] == 1).
     rewrite eq_sym; apply: leif_eq.
     have N_G: '[G] \in Num.nat.
@@ -2147,9 +2147,9 @@ have [Gamma [S4_Gamma normGamma [b Dbeta]]]:
       congr (_ + _); rewrite dB scaleNr [- _ + _]addrC cfnormB !cfnormZ.
       rewrite normr_nat intr_normK // scaler_sumr cfdotZr rmorph_nat.
       rewrite cfnorm_map_orthonormal // cfproj_sum_orthonormal //.
-      rewrite Itau1 ?mem_zchar// n1psi1 mulr1 rmorphM/= rmorph_nat conj_intr //.
-      rewrite -mulr2n oS1ua -muln_divA // mul2n -addrA addrCA -natrX mulrBl.
-      by congr (_ + (_ - _)); rewrite -mulrnAl -mulrnA muln2 mulrC.
+      rewrite Itau1 ?mem_zchar// n1psi1 mulr1 [conjC _]rmorphM/= rmorph_nat.
+      rewrite conj_intr // -mulr2n oS1ua -muln_divA // -addrA addrCA mulrBl.
+      by rewrite -mulrnAl -mulrnA mul2n muln2 -natrX [b * _]mulrC.
     rewrite Itau // cfnormBd; last first.
       by rewrite cfdotZr oSS ?mulr0 // (memPnC S1'lam1).
     by rewrite cfnormZ normr_nat n1psi1 n1lam1 mulr1 addrC -natrX.