proposition: Lemma subidP m n (I : 'cV[R]_m) (J : 'cV[R]_n) : reflect (exists D, I = D *m J) (I <= J)%IS.
proof: Proof. apply: (iffP ('forall_(memberP _ _))); last first. move=> [D ->] i; exists (row i D). apply/matrixP => i' j'; rewrite !ord1 {i' j'} !mxE /=. by apply: eq_bigr => l _; rewrite !mxE. move=> HJ; pose M i j := projT1 (sig_eqW (HJ i)) 0 j. exists (\matrix_(i,j) M i j); apply/colP => i; rewrite mxE. transitivity (\sum_j M i j * J j 0); last first. by apply: eq_bigr => j _ /=; rewrite mxE. rewrite /M {M}; case: sig_eqW => //= K. by move=> /matrixP /(_ 0 0); rewrite !mxE eqxx mulr1n. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice fingroup) mathcomp(matrix bigop zmodp mxalgebra poly) ssrcomplements