proposition: Fact Crat_span_subproof s x : decidable (in_Crat_span s x).
proof: Proof. have [Qxs [QxsC [[|x1 s1] // [<- <-] {x s} _]]] := num_field_exists (x :: s). have QxsC_Z a zz: QxsC (a *: zz) = QtoC a * QxsC zz. rewrite mulrAC; apply: (canRL (mulfK _)); first by rewrite intr_eq0 denq_eq0. by rewrite mulrzr mulrzl -!rmorphMz scalerMzl -mulrzr -numqE scaler_int. apply: decP (x1 \in <<in_tuple s1>>%VS) _; rewrite /in_Crat_span size_map. apply: (iffP idP) => [/coord_span-> | [a Dx]]. move: (coord _) => a; exists [ffun i => a i x1]; rewrite rmorph_sum /=. by apply: eq_bigr => i _; rewrite ffunE (nth_map 0). have{Dx} ->: x1 = \sum_i a i *: s1`_i. apply: (fmorph_inj QxsC); rewrite Dx rmorph_sum /=. by apply: eq_bigr => i _; rewrite QxsC_Z (nth_map 0). by apply: memv_suml => i _; rewrite memvZ ?memv_span ?mem_nth. 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)