proposition: Lemma kerP m n k (M : 'M[R]_(m,n)) (X : 'M_(k, m)) : reflect (exists Y : 'M_(k, dim_ker M), X = Y *m ker M) (X *m M == 0).
proof: Proof. apply: (iffP eqP); last first. case=> [Y ->]; apply/row_matrixP => i. by rewrite !row_mul row0 kerAK. move=> XM0; have XM0_ i : row i X *m M == 0 by rewrite -row_mul XM0 row0. exists (\matrix_(i, j) (projT1 (sig_eqW (kerP_subproof _ _ _ _ (XM0_ i)))) 0 j). by apply/row_matrixP => i; rewrite row_mul rowK; case: sig_eqW. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice matrix bigop zmodp mxalgebra poly) ssrcomplements dvdring stronglydiscrete