proposition: Lemma maxrowsub_free : row_free (rowsub mxf A).
proof: Proof. rewrite /mxf; case: arg_maxnP => //= f _ fM; apply/negP => /negP rfA. have [i NriA] : exists i, ~~ (row i A <= rowsub f A)%MS. by apply/row_subPn; apply: contraNN rfA => /mxrankS; rewrite row_leq_rank. have [j rjfA] : exists j, (row (f j) A <= rowsub (f \o lift j) A)%MS. case/row_freePn: rfA => j. by rewrite row_rowsub row'Esub -mxsub_comp; exists j. pose g : 'I_m ^ \rank A := finfun [eta f with j |-> i]. suff: (rowsub f A < rowsub g A)%MS by rewrite ltmxErank andbC ltnNge fM. rewrite ltmxE; apply/andP; split; last first. apply: contra NriA; apply: submx_trans. by rewrite (eq_row_sub j)// row_rowsub ffunE/= eqxx. apply/row_subP => k; rewrite !row_rowsub. have [->|/negPf eq_kjF] := eqVneq k j; last first. by rewrite (eq_row_sub k)// row_rowsub ffunE/= eq_kjF. rewrite (submx_trans rjfA)// (submx_rowsub (lift j))// => l /=. by rewrite ffunE/= eq_sym (negPf (neq_lift _ _)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)