proposition: Lemma restr_perm_inj s : {in porbit_set s &, injective ((restr_perm (T:=T))^~ s)}.
proof: Proof. Proof using. by move=> C D /psupport_restr_perm {2}<- /psupport_restr_perm {2}<- ->. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple path bigop finset div) mathcomp(fingroup perm action ssralg) tools permcomp