proposition: Lemma permKP s : reflect (involutive s) (s^-1 == s).
proof: Proof. apply (iffP eqP) => [ssV i | invs]. - by rewrite -{1}ssV permK. - rewrite -permP => i; apply (@perm_inj _ s). by rewrite invs permKV. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype div) mathcomp(finset fingroup perm morphism action)