proposition: Lemma row_thin_mx p q (M : 'M_(p,0)) (N : 'M[T]_(p,q)) : row_mx M N = N.
proof: Proof. apply/matrixP=> i j; rewrite mxE; case: splitP=> [|k H]; first by case. by congr fun_of_matrix; exact: val_inj. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype finfun perm matrix bigop zmodp mxalgebra) mathcomp(choice poly polydiv mxpoly binomial)