proposition: Lemma lines_scale_row m n a (M: 'M[R]_(m,n)): forall s, uniq s -> (forall i, i \in s -> row i (foldl (fun N i => line_scale i a N) M s) = a *: row i M) /\ (forall i, i \notin s -> row i (foldl (fun N i => line_scale i a N) M s) = row i M).
proof: Proof. move => s. elim : s n M => [ | hd tl hi] //= n M /andP [h1 h2]. split => i; rewrite in_cons. - move/orP => [/eqP{i}-> | hin]. + case: (hi _ (line_scale hd a M) h2) => _ hr. by rewrite hr // line_scale_row_eq. case: (hi _ (line_scale hd a M) h2) => -> // _. rewrite line_scale_row_neq //. by apply: contraNneq h1 => ->. rewrite negb_or => /andP[hl hr]. case: (hi _ (line_scale hd a M) h2) => _ hR. by rewrite hR // line_scale_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)