proposition: Fact dvdA_zmod_closed e : zmod_closed (dvdA e).
proof: Proof. split=> [|x y]; first by rewrite unfold_in mul0r eqxx rpred0 ?if_same. rewrite ![(e %| _)%A]unfold_in. case: ifP => [_ x0 /eqP-> | _]; first by rewrite subr0. by rewrite mulrBl; apply: rpredB. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv ssrnum ssrint archimedean rat) mathcomp(finalg zmodp matrix mxalgebra mxpoly vector intdiv) mathcomp(falgebra fieldext separable galois algC cyclotomic)