proposition: Lemma key_lemma m d l (c : 'cV[R]_m) M : d ^+ m * \det (block_mx d%:M l c M) = d * \det (d *: M - c *m l).
proof: Proof. rewrite -[d ^+ m]mul1r -det_scalar -(det1 _ 1) -(det_ublock _ 0) -det_mulmx. rewrite mulmx_block ?(mul0mx,addr0,add0r,mul1mx,mul_scalar_mx) -2![LHS]mul1r. rewrite -{1}(@det1 _ 1) -{2}(@det1 _ m) mulrA -(@det_lblock _ _ _ _ (- c)). rewrite -det_mulmx mulmx_block ?(mul1mx,mul0mx,addr0) addrC mul_mx_scalar. by rewrite scalerN subrr det_ublock det_scalar1 addrC mulNmx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path ssralg) mathcomp(fintype perm choice matrix bigop zmodp poly polydiv mxpoly) CoqEAL(minor hrel param refinements seqmx)