proposition: Lemma minor_lift_block m n p (f1 : 'I_p -> 'I_m) (f2 : 'I_p -> 'I_n) a (M : 'M[R]_(m,n)) (l : 'rV[R]_n) : minor (lift_pred f1) (lift_pred f2) (block_mx a%:M l 0 M) = a * minor f1 f2 M.
proof: Proof. by rewrite /minor submatrix_lift_block submatrix0 (@det_ublock _ 1) det_scalar1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path ssralg) mathcomp(fintype perm choice finfun matrix bigop zmodp poly mxpoly)