proposition: Lemma Cint_spanP n (s : n.-tuple algC) x : reflect (inIntSpan s x) (x \in Cint_span s).
proof: Proof. rewrite unfold_in; case: (dec_Cint_span _ _) => [Zs_x | Zs'x] /=. left; have{Zs_x} [] := Zs_x; rewrite /= size_map size_tuple => a /rowP/(_ 0). rewrite !mxE => ->; exists a; rewrite summxE; apply: eq_bigr => i _. by rewrite -scaler_int (nth_map 0) ?size_tuple // !mxE mulrzl. right=> [[a Dx]]; have{Zs'x} [] := Zs'x. rewrite /inIntSpan /= size_map size_tuple; exists a. apply/rowP=> i0; rewrite !mxE summxE Dx; apply: eq_bigr => i _. by rewrite -scaler_int mxE mulrzl (nth_map 0) ?size_tuple // !mxE. 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)