Enriched numClosedFieldType so that it factors a lot of theory from both complex and algC.

The definitions of 'i, conjC, Re, Im, n.-root, sqrtC and their theory
have been moved to the numClosedFieldType structure in ssrnum.
This covers boths the uses in algC and complex.v. To that end the
numClosedFieldType structure has been enriched with conjugation and 'i.
Note that 'i can be deduced from the property of algebraic closure and is
only here to let the user chose which definitional equality should hold
on 'i. Same thing for conjC that could be written  `|x|^+2/x, the only
nontrivial (up to my knowledge) property is the fact that conjugation
is a ring morphism.

1 files changed, 3 insertions, 3 deletions

diff --git a/mathcomp/odd_order/PFsection6.v b/mathcomp/odd_order/PFsection6.v
index 6d9ecfc..cbde798 100644
--- a/mathcomp/odd_order/PFsection6.v
+++ b/mathcomp/odd_order/PFsection6.v
@@ -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).