proposition: Lemma ractpermE : actperm (to \ sAD) =1 actperm to.
proof: Proof. by move=> a; apply/permP=> x; rewrite !permE. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)