proposition: Lemma col_matrix (R : ringType) m n (A : 'I_m -> 'cV[R]_(n.+1)) (i : 'I_m) : col i (\matrix_(a < n.+1, b < m) (A b) a ord0) = A i.
proof: Proof. apply/colP => a; by rewrite !mxE. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2