proposition: Lemma disjoint_psupports_conjg (A : {set {perm T}}) a : disjoint_psupports A -> disjoint_psupports [set (s ^ a)%g | s in A].
proof: Proof. Proof using. move => [/trivIsetP Hdisj Hinj]. split => [|x1 x2 /imsetP[s1 Hs1 ->] /imsetP[s2 Hs2 ->]]. - apply /trivIsetP => B1 B2. move => /imsetP[x1 /imsetP[s1 Hs1 ->] ->{x1}]. move => /imsetP[x2 /imsetP[s2 Hs2 ->] ->{x2}]. rewrite !psupport_conjg => Hdiff. apply disjoint_imset; first exact: perm_inj. apply: Hdisj; try exact: imset_f. by move: Hdiff; apply contra => /eqP ->. - rewrite !psupport_conjg => Hsupp. rewrite (_ : s1 = s2) //; apply Hinj => //. apply /setP => x; apply /idP/idP => Hx. + have:= imset_f a Hx. by rewrite Hsupp => /imsetP[y Hy /perm_inj ->]. + have:= imset_f a Hx. by rewrite -Hsupp => /imsetP[y Hy /perm_inj ->]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(tuple finfun finset path bigop) mathcomp(fingroup perm action) mathcomp(ssralg matrix mxalgebra algC classfun) partition tools sorted permcomp fibered_set cycles