fact: Definition morph_act rT rT' (to : action D rT) (to' : action D' rT') f fA := forall x a, f (to x a) = to' (f x) (fA a).
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)