proposition: Lemma mx_series_rcons U V : mx_series (rcons U V) <-> [/\ mx_series U, modG V & max_submod (last 0 U) V].
proof: Proof. rewrite /mx_series /mx_subseries all_rcons size_rcons -rcons_cons. split=> [ [/andP[modU modV] maxU] | [[modU maxU] modV maxV]]. split=> //; last first. by have:= maxU _ (leqnn _); rewrite !nth_rcons leqnn ltnn eqxx -last_nth. by split=> // i ltiU; have:= maxU i (ltnW ltiU); rewrite !nth_rcons leqW ltiU. rewrite modV; split=> // i; rewrite !nth_rcons ltnS leq_eqVlt. case: eqP => [-> _ | /= _ ltiU]; first by rewrite ltnn ?eqxx -last_nth. by rewrite ltiU; apply: maxU. 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)