proposition: Lemma subset_faithful A B S : B \subset A -> [faithful A, on S | to] -> [faithful B, on S | to].
proof: Proof. by move=> sAB; apply: subset_trans; apply: setSI. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)