proposition: Corollary Aint_subring : subring_closed Aint.
proof: Proof. suff rAZ: {in Aint &, forall x y, (x - y \in Aint) * (x * y \in Aint)}. by split=> // x y AZx AZy; rewrite rAZ. move=> x y AZx AZy. have [|S [ringS] ] := @Aint_subring_exists [:: x; y]; first exact/allP/and3P. move=> /allP/and3P[Sx Sy _] [Y _ genYS]. have AZ_S := fin_Csubring_Aint ringS genYS. by have [_ S_B S_M] := ringS; rewrite !AZ_S ?S_B ?S_M. 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)