proposition: Lemma line_comb_row_neq n m k k' l a (M: 'M[R]_(n,m)): k != k' -> row k' (line_comb k l a M) = row k' M.
proof: Proof. move/negbTE => hkk'. by apply/rowP => i; rewrite !mxE eq_sym hkk' !mxE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(ssralg fintype perm choice) mathcomp(matrix bigop zmodp mxalgebra poly mxpoly)