proposition: Lemma key_lemma_sub m n k (M : 'M[R]_(1 + m,1 + n)) (f : 'I_k -> 'I_m) (g : 'I_k -> 'I_n) : M 0 0 * (minor f g (M 0 0 *: drsubmx M - dlsubmx M *m ursubmx M)) = M 0 0 ^+ k * (minor (lift_pred f) (lift_pred g) M).
proof: Proof. rewrite /minor -{7}[M]submxK submatrix_add submatrix_scale submatrix_opp. have -> : ulsubmx M = (M 0 0)%:M by apply/rowP=> i; rewrite ord1 !mxE !lshift0. by rewrite submatrix_lift_block key_lemma submatrix_mul. 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)