addressing comments about PR#221 of mathcomp

1 files changed, 22 insertions, 25 deletions

diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v
index 651dd6d..9631d28 100644
--- a/mathcomp/fingroup/action.v
+++ b/mathcomp/fingroup/action.v
@@ -1607,7 +1607,7 @@ Qed.
 
 Canonical perm_action := Action aperm_is_action.
 
-Lemma pcycleE a : pcycle a = orbit perm_action <[a]>%g.
+Lemma porbitE a : porbit a = orbit perm_action <[a]>%g.
 Proof. by []. Qed.
 
 Lemma perm_act1P a : reflect (forall x, aperm x a = x) (a == 1).
@@ -1643,11 +1643,11 @@ move=> sAD x; rewrite morphimEsub // /orbit -imset_comp.
 by apply: eq_imset => a //=; rewrite actpermK.
 Qed.
 
-Lemma pcycle_actperm (a : aT) :
-   a \in D -> pcycle (actperm to a) =1 orbit to <[a]>.
+Lemma porbit_actperm (a : aT) :
+   a \in D -> porbit (actperm to a) =1 orbit to <[a]>.
 Proof.
 move=> Da x.
-by rewrite pcycleE -orbit_morphim_actperm ?cycle_subG ?morphim_cycle.
+by rewrite porbitE -orbit_morphim_actperm ?cycle_subG ?morphim_cycle.
 Qed.
 
 End ActpermOrbits.
@@ -1680,26 +1680,8 @@ Proof. by rewrite ker_actperm astab_actby setIT (setIidPr (astab_sub _ _)). Qed.
 Lemma im_restr_perm p : restr_perm p @: S = S.
 Proof. exact: im_perm_on (restr_perm_on p). Qed.
 
-Definition perm_ong : {set {perm T}} := [set s | perm_on S s].
-Lemma group_set_perm_ong : group_set perm_ong.
-Proof using.
-apply/group_setP; split => [| s t]; rewrite !inE;
-   [exact: perm_on1 | exact: perm_onM].
-Qed.
-Canonical perm_ong_group : {group {perm T}} := Group group_set_perm_ong.
-Lemma card_perm_ong : #|perm_ong| = #|S|`!.
-Proof using. by rewrite cardsE /= card_perm. Qed.
-
-Lemma perm_ongE : perm_ong = 'C(~:S | 'P).
-Proof using.
-apply/setP => s; rewrite inE; apply/idP/astabP => [Hperm x | Hstab].
-- by rewrite inE /= apermE => /out_perm; apply.
-- apply/subsetP => x; rewrite unfold_in; apply contraR => H.
-  by move/(_ x): Hstab; rewrite inE /= apermE => ->.
-Qed.
-
 Lemma restr_perm_commute s : commute (restr_perm s) s.
-Proof using.
+Proof.
 case: (boolP (s \in 'N(S | 'P))) =>
     [HC | /triv_restr_perm ->]; last exact: (commute_sym (commute1 _)).
 apply/permP => x; case: (boolP (x \in S)) => Hx; rewrite !permM.
@@ -1711,6 +1693,19 @@ Qed.
 
 End RestrictPerm.
 
+Section Symmetry.
+
+Variables (T : finType) (S : {set T}).
+
+Lemma SymE : Sym S = 'C(~: S | 'P).
+Proof.
+apply/setP => s; rewrite inE; apply/idP/astabP => [Hperm x | Hstab].
+- by rewrite inE /= apermE => /out_perm; apply.
+- apply/subsetP => x; rewrite unfold_in; apply contraR => H.
+  by move/(_ x): Hstab; rewrite inE /= apermE => ->.
+Qed.
+
+End Symmetry.
 
 Section AutIn.
 
@@ -2403,7 +2398,7 @@ exact: (morph_afix (gact_stable to1) (injmP injh)).
 Qed.
 
 Lemma morph_gact_irr A M :
-    A \subset D1 -> M \subset R1 -> 
+    A \subset D1 -> M \subset R1 ->
   acts_irreducibly (f @* A) (h @* M) to2 = acts_irreducibly A M to1.
 Proof.
 move=> sAD1 sMR1.
@@ -2737,4 +2732,6 @@ Arguments aut_groupAction {gT} G%g.
 Notation "[ 'Aut' G ]" := (aut_action G) : action_scope.
 Notation "[ 'Aut' G ]" := (aut_groupAction G) : groupAction_scope.
 
-
+Notation pcycleE := (deprecate pcycleE porbitE _) (only parsing).
+Notation pcycle_actperm := (deprecate pcycle_actperm porbit_actperm _)
+  (only parsing).