proposition: Theorem mx_Schreier U : mx_subseries U -> path ltmx 0 U -> classically (exists V, [/\ mx_series V, last 0 V :=: 1%:M & subseq U V])%MS.
proof: Proof. move: U => U0; set U := {1 2}U0; have: subseq U0 U := subseq_refl U. pose n' := n.+1; have: n < size U + n' by rewrite leq_addl. elim: n' U => [|n' IH_U] U ltUn' sU0U modU incU [] // noV. rewrite addn0 ltnNge in ltUn'; case/negP: ltUn'. by rewrite (leq_trans (max_size_mx_series incU)) ?rank_leq_row. apply: (noV); exists U; split => //; first split=> // i lt_iU; last first. apply/eqmxP; apply: contraT => neU1. apply: {IH_U}(IH_U (rcons U 1%:M)) noV. - by rewrite size_rcons addSnnS. - by rewrite (subseq_trans sU0U) ?subseq_rcons. - by rewrite /mx_subseries all_rcons mxmodule1. by rewrite rcons_path ltmxEneq neU1 submx1 !andbT. set U'i := _`_i; set Ui := _`_i; have defU := cat_take_drop i U. have defU'i: U'i = last 0 (take i U). rewrite (last_nth 0) /U'i -{1}defU -cat_cons nth_cat /=. by rewrite size_take lt_iU leqnn. move: incU; rewrite -defU cat_path (drop_nth 0) //= -/Ui -defU'i. set U' := take i U; set U'' := drop _ U; case/and3P=> incU' ltUi incU''. split=> // W [modW ltUW ltWV]; case: notF. apply: {IH_U}(IH_U (U' ++ W :: Ui :: U'')) noV; last 2 first. - by rewrite /mx_subseries -drop_nth // all_cat /= modW -all_cat defU. - by rewrite cat_path /= -defU'i; apply/and4P. - by rewrite -drop_nth // size_cat /= addnS -size_cat defU addSnnS. by rewrite (subseq_trans sU0U) // -defU cat_subseq // -drop_nth ?subseq_cons. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)