proposition: Lemma perm_on_id u S : perm_on S u -> #|S| <= 1 -> u = 1%g.
proof: Proof. rewrite leq_eqVlt ltnS leqn0 => pSu S10; apply/permP => t; rewrite perm1. case/orP : S10; last first. by move/eqP/cards0_eq => S0; apply: (out_perm pSu); rewrite S0 inE. move=> /cards1P[x Sx]. have [-> | ntx] := eqVneq t x; last by apply: (out_perm pSu); rewrite Sx inE. by apply/eqP; have := perm_closed x pSu; rewrite Sx !inE => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)