proposition: Lemma max_size_mx_series (V : seq 'M[F]_n) : path ltmx 0 V -> size V <= \rank (last 0 V).
proof: Proof. rewrite -[size V]addn0 -(mxrank0 F n n); elim: V 0 => //= V1 V IHV V0. rewrite ltmxErank -andbA => /and3P[_ ltV01 ltV]. by apply: leq_trans (IHV _ ltV); rewrite addSnnS leq_add2l. 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)