proposition: Lemma subgen_coherent S1 S2 A tau: {subset S2 <= 'Z[S1]} -> coherent S1 A tau -> coherent S2 A tau.
proof: Proof. move/zchar_trans=> sS21 [tau1 [[Itau1 Ztau1] def_tau]]. exists tau1; split; last exact: sub_in1 def_tau. by split; [apply: sub_in2 Itau1 | apply: sub_in1 Ztau1]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action zmodp) mathcomp(gfunctor gproduct cyclic pgroup frobenius) mathcomp(matrix mxalgebra mxrepresentation vector ssrint) mathcomp(ssrnum algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4)