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