diff options
| author | Georges Gonthier | 2015-11-30 17:15:40 +0000 |
|---|---|---|
| committer | Georges Gonthier | 2015-12-04 15:07:16 +0000 |
| commit | 7737563121b069ab5e15f1f8ddf2533d3fef1434 (patch) | |
| tree | fb718c2e7929e0599d56f24068de2dc0d5c6f323 /mathcomp | |
| parent | 0b227098257e188bdb59e59e63b24e392e21dd87 (diff) | |
Removed spurious injection & clean up proof
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/solvable/maximal.v | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index 9865264..098a325 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.v @@ -411,12 +411,11 @@ case Gp: (p \in \pi(G)); last first. rewrite card1_trivg ?sub1G // (card_Hall sylP). rewrite part_p'nat // (pnat_dvd (cardSg (normal_sub nsHG))) //. by rewrite /pnat cardG_gt0 all_predC has_pred1 Gp. -have{P sylP}[-> //] := nilpotent_Hall_pcore nilH sylP. +rewrite {P sylP}(nilpotent_Hall_pcore nilH sylP). rewrite -(bigdprodWY (erefl 'F(G))) sub_gen //. rewrite -(filter_pi_of (ltnSn _)) big_filter big_mkord. -have le_pG: p < #|G|.+1. - by rewrite ltnS dvdn_leq //; move: Gp; rewrite mem_primes => /and3P[]. -apply: (bigcup_max (Ordinal le_pG)) => //=. +apply: (bigcup_max (Sub p _)) => //= [|_]. + by have:= Gp; rewrite ltnS mem_primes => /and3P[_ ntG /dvdn_leq->]. by rewrite pcore_max ?pcore_pgroup ?gFnormal_trans. Qed. |