proposition: Lemma Aint_subring_exists (X : seq algC) : {subset X <= Aint} -> {S : pred algC & subring_closed S /\ {subset X <= S} & {Y : {n : nat & n.-tuple algC} & {subset tagged Y <= S} & forall x, reflect (inIntSpan (tagged Y) x) (x \in S)}}.
proof: Proof. move=> AZ_X; pose m := (size X).+1. pose n (i : 'I_m) := (size (minCpoly X`_i)).-2; pose N := (\max_i n i).+1. pose IY := family (fun i => [pred e : 'I_N | e <= n i]%N). have IY_0: 0 \in IY by apply/familyP=> // i; rewrite ffunE. pose inIY := enum_rank_in IY_0. pose Y := [seq \prod_(i < m) X`_i ^+ (f : 'I_N ^ m) i | f in IY]. have S_P := Cint_spanP [tuple of Y]; set S := Cint_span _ in S_P. have sYS: {subset Y <= S} by apply: mem_Cint_span. have S_1: 1 \in S. by apply/sYS/imageP; exists 0 => //; rewrite big1 // => i; rewrite ffunE. have SmulX (i : 'I_m): {in S, forall x, x * X`_i \in S}. move=> _ /S_P[x ->]; rewrite mulr_suml rpred_sum // => j _. rewrite mulrzAl rpredMz {x}// nth_image mulrC (bigD1 i) //= mulrA -exprS. move: {j}(enum_val j) (familyP (enum_valP j)) => f fP. have:= fP i; rewrite inE /= leq_eqVlt => /predU1P[-> | fi_ltn]; last first. apply/sYS/imageP; have fiK: (inord (f i).+1 : 'I_N) = (f i).+1 :> nat. by rewrite inordK // ltnS (bigmax_sup i). exists (finfun [eta f with i |-> inord (f i).+1]). apply/familyP=> i1; rewrite inE ffunE /= fun_if fiK. by case: eqP => [-> // | _]; apply: fP. rewrite (bigD1 i isT) ffunE /= eqxx fiK; congr (_ * _). by apply: eq_bigr => i1 /[!ffunE]/= /negPf->. have [/monicP ] := (minCpoly_monic X`_i, root_minCpoly X`_i). rewrite /root horner_coef lead_coefE -(subnKC (size_minCpoly _)) subn2. rewrite big_ord_recr /= addrC addr_eq0 => ->; rewrite mul1r => /eqP->. have /floorpP[p Dp]: X`_i \in Aint. by have [/(nth_default 0)-> | /(mem_nth 0)/AZ_X] := leqP (size X) i. rewrite -/(n i) Dp mulNr rpredN // mulr_suml rpred_sum // => [[e le_e]] /= _. rewrite coef_map -mulrA mulrzl rpredMz ?sYS //; apply/imageP. have eK: (inord e : 'I_N) = e :> nat by rewrite inordK // ltnS (bigmax_sup i). exists (finfun [eta f with i |-> inord e]). apply/familyP=> i1; rewrite inE ffunE /= fun_if eK. by case: eqP => [-> // | _]; apply: fP. rewrite (bigD1 i isT) ffunE /= eqxx eK; congr (_ * _). by apply: eq_bigr => i1 /[!ffunE] /= /negPf->. exists S; last by exists (Tagged (fun n => n.-tuple _) [tuple of Y]). split=> [|x Xx]; last first. by rewrite -[x]mul1r -(nth_index 0 Xx) (SmulX (Ordinal _)) // ltnS index_size. split=> // x y Sx Sy; first by rewrite rpredB. case/S_P: Sy => {y}[y ->]; rewrite mulr_sumr rpred_sum //= => j. rewrite mulrzAr rpredMz {y}// nth_image; move: {j}(enum_val j) => f. elim/big_rec: _ => [|i y _ IHy] in x Sx *; first by rewrite mulr1. rewrite mulrA {y}IHy //. elim: {f}(f i : nat) => [|e IHe] in x Sx *; first by rewrite mulr1. by rewrite exprS mulrA IHe // SmulX. 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)