proposition: Lemma lines_comb_row m n a l (M: 'M[R]_(m,n)): forall s, uniq s -> l \notin s -> (forall i, i \in s -> row i (foldl (fun N i => line_comb i l a N) M s) = row i M + a *: row l M) /\ (forall i, i \notin s -> row i (foldl (fun N i => line_comb i l a N) M s) = row i M).
proof: Proof. move => s. elim : s M => [ | hd tl hi] //= M /andP [h1 h2]. rewrite in_cons negb_or => /andP [hl1 hl2]. split => i; rewrite in_cons. - move/orP => [/eqP{i}-> | hin]. + case: (hi (line_comb hd l a M) h2 hl2) => _ hr. by rewrite hr // line_comb_row_eq. case: (hi (line_comb hd l a M) h2 hl2) => -> // _. rewrite !line_comb_row_neq // eq_sym // eq_sym. by apply: contraNneq h1 => ->. rewrite negb_or => /andP [hl hr]. case: (hi (line_comb hd l a M) h2 hl2) => _ hR. by rewrite hR // !line_comb_row_neq // eq_sym. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(ssralg fintype perm choice) mathcomp(matrix bigop zmodp mxalgebra poly mxpoly)