proposition: Lemma det_lines_comb_dep m (a: 'I_m -> R) l (M: 'M[R]_m) s: l \notin s -> \det (foldl (fun N i => line_comb i l (a i) N) M s) = \det M.
proof: Proof. elim : s M => [ | hd tl hi] M //=. rewrite in_cons negb_or => /andP [hl1 hl2]. by rewrite hi // det_line_comb // eq_sym. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(ssralg fintype perm choice) mathcomp(matrix bigop zmodp mxalgebra poly mxpoly)