proposition: Lemma submatrix_scalar_mx m p (f : 'I_p -> 'I_m) (hf : injective f) (a : R) : submatrix f f a%:M = a%:M.
proof: Proof. apply/matrixP => i j; rewrite !mxE. case h : (f i == f j); first by rewrite (hf _ _ (eqP h)) eqxx. by case h': (i == j) => //; move: h; rewrite (eqP h') eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path ssralg) mathcomp(fintype perm choice finfun matrix bigop zmodp poly mxpoly)