diff options
| author | Cyril Cohen | 2018-02-06 19:36:53 +0100 |
|---|---|---|
| committer | GitHub | 2018-02-06 19:36:53 +0100 |
| commit | d6bc72cd477ed6fe8b95782b26a2e0fc92711395 (patch) | |
| tree | 6996e39182b97573b1cdecaeb7c8c8a3f58c1e77 /mathcomp/odd_order/PFsection8.v | |
| parent | 11e539dae1bfe8bc67fc7bd1eb65ee3b4c29f813 (diff) | |
| parent | f3ce9ace4b55654d6240db9eb41a6de3c488f0d9 (diff) | |
Merge pull request #164 from CohenCyril/linting
linting of 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. |