proposition: Lemma blockE00 m n d (l: 'rV[R]_n) (c: 'cV[R]_m) (M: 'M[R]_(m,n)): (block_mx d%:M l c M) 0 0 = d.
proof: Proof. rewrite !mxE. case: splitP => x //; rewrite [x]ord1 {x} !mxE => _. by case: splitP => x //; rewrite [x]ord1 {x} !mxE => _. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path ssralg) mathcomp(fintype perm choice matrix bigop zmodp poly polydiv mxpoly) CoqEAL(ssrcomplements minor dvdring) polydvd