proposition: Lemma rank_row_mx n (A : 'M[F]_n) m (B : 'M[F]_(n, m)) : \rank A = n -> \rank (row_mx A B) = n.
proof: Proof. move=> HA. apply/eqP. apply/row_freeP. exists (col_mx ((invmx (row_ebase A)) *m (invmx (col_ebase A))) 0). rewrite mul_row_col mulmx0 addr0 -{1}(mulmx_ebase A) HA pid_mx_1 mulmx1 -!mulmxA. have -> : row_ebase A *m (invmx (row_ebase A) *m invmx (col_ebase A)) = invmx (col_ebase A). rewrite !mulmxA mulmxV. by rewrite mul1mx. by apply: row_ebase_unit. rewrite mulmxV //. by apply: col_ebase_unit. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2