diff options
| author | Cyril Cohen | 2017-11-23 16:33:36 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2018-02-06 13:54:37 +0100 |
| commit | fafd4dac5315e1d4e071b0044a50a16360b31964 (patch) | |
| tree | 5b66c3d67e2b146e3a8013496379b96dd60dc75a /mathcomp/odd_order/PFsection8.v | |
| parent | 835467324db450c8fb8971e477cc4d82fa3e861b (diff) | |
running semi-automated linting on the whole library
Diffstat (limited to 'mathcomp/odd_order/PFsection8.v')
| -rw-r--r-- | mathcomp/odd_order/PFsection8.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/odd_order/PFsection8.v b/mathcomp/odd_order/PFsection8.v index d4ffa46..2770369 100644 --- a/mathcomp/odd_order/PFsection8.v +++ b/mathcomp/odd_order/PFsection8.v @@ -557,7 +557,7 @@ have [part_a _ _ [part_b part_c]] := BGsummaryB maxM complU. rewrite eqEsubset FTsupp1_sub // andbT -setD_eq0 in part_c. split=> // X notX0 /subsetD1P[sXU notX1]; rewrite -cent_gen defH. apply: part_b; rewrite -?subG1 ?gen_subG //. -by rewrite -setD_eq0 setDE (setIidPl _) // subsetC sub1set inE. +by rewrite -setD_eq0 setDE (setIidPl _) // subsetC sub1set inE. Qed. (* This is Peterfalvi (8.13). *) @@ -1111,7 +1111,7 @@ without loss{suppST} suppST: T maxT ncST / FTsupports S T. have{suppST} [y /and3P[ASy not_sCyS sCyT]] := existsP suppST. have Dy: y \in [set z in 'A0(S) | ~~ ('C[z] \subset S)] by rewrite !inE ASy. have [_ [_ /(_ y Dy) uCy] /(_ y Dy)[_ coTcS _ typeT]] := FTsupport_facts maxS. -rewrite -mem_iota -(eq_uniq_mmax uCy maxT sCyT) !inE in coTcS typeT. +rewrite -mem_iota -(eq_uniq_mmax uCy maxT sCyT) !inE in coTcS typeT. apply/negbNE; rewrite -part_b /NC 1?orbit_sym // negb_exists. apply/forallP=> x; rewrite part_a1 ?mmaxJ ?negbK //; last first. by rewrite /NC (orbit_transl _ (mem_orbit _ _ _)) ?in_setT // orbit_sym. |