proposition: Lemma mem_Crat_span s : {subset s <= Crat_span s}.
proof: Proof. move=> _ /(nthP 0)[ix ltxs <-]; pose i0 := Ordinal ltxs. apply/Crat_spanP; exists [ffun i => (i == i0)%:R]. rewrite (bigD1_ord i0) //= ffunE eqxx // rmorph1 mul1r. by rewrite big1 ?addr0 // => i; rewrite ffunE rmorph_nat mulr_natl lift_eqF. 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)