proposition: Lemma blockE0i m n d (l: 'rV[R]_n) (c: 'cV[R]_m) (M: 'M[R]_(m,n)) i: (block_mx d%:M l c M) 0 (lift 0 i) = (l 0 i).
proof: Proof. rewrite !mxE. case: splitP => x //; rewrite [x]ord1 {x} !mxE => _. case: splitP => x; first by rewrite [x]ord1. by rewrite /= /bump /leq0n => /eqP; rewrite eqSS => /eqP/ord_inj->. 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