From 19ac0629d643f85ed1ec2db86f991c848ef3bbbd Mon Sep 17 00:00:00 2001 From: Georges Gonthier Date: Thu, 3 Dec 2015 15:33:38 +0000 Subject: [PATCH] Remove spurious injections --- mathcomp/odd_order/BGsection15.v | 4 +--- mathcomp/odd_order/BGsection16.v | 2 +- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/mathcomp/odd_order/BGsection15.v b/mathcomp/odd_order/BGsection15.v index 971a2c8d63..553feda9dc 100644 --- a/mathcomp/odd_order/BGsection15.v +++ b/mathcomp/odd_order/BGsection15.v @@ -1248,7 +1248,7 @@ Lemma nonTI_Fitting_facts M : [/\ M \in 'M_'F :|: 'M_'P1, M`_\F = M`_\sigma & M^`(1) \subset 'F(M)]. Proof. move=> maxM nonTI; suff: [exists (y | y \notin M), 'F(M) :&: 'F(M) :^ y != 1]. - by case/exists_inP=> y notMy /nonTI_Fitting_structure[] // [[-> ?] _ []]. + by case/exists_inP=> y notMy /nonTI_Fitting_structure[] // [-> dMF] _ []. rewrite -negb_forall_in; apply: contra nonTI => /forall_inP tiF. apply/normedTI_P; rewrite normD1 setTI gFnorm setD_eq0 subG1. split=> // [|g _]; first by rewrite (trivg_Fitting (mmax_sol maxM)) mmax_neq1. @@ -1509,5 +1509,3 @@ by rewrite (subG1_contra _ ntCMsx) ?setIS //= -cent_cycle centS. Qed. End Section15. - - diff --git a/mathcomp/odd_order/BGsection16.v b/mathcomp/odd_order/BGsection16.v index 3f0cf92984..32850e48cb 100644 --- a/mathcomp/odd_order/BGsection16.v +++ b/mathcomp/odd_order/BGsection16.v @@ -786,7 +786,7 @@ split; first by have [_ _ _ _ []] := Ptype_structure PmaxM hallK. have [<- | neqMF_Ms] := eqVneq M`_\F M`_\sigma; first exact: Fcore_sub_Fitting. have solMs: solvable M`_\sigma := solvableS (pcore_sub _ _) (mmax_sol maxM). have [D hallD] := Hall_exists #|Kstar|^' solMs. -by case: (Fcore_structure maxM) notP1maxM => _ /(_ K D)[] // [[->]]. +by case: (Fcore_structure maxM) notP1maxM => _ /(_ K D)[] // [->]. Qed. End SingleGroupSummaries.