proposition: Lemma ker_cP : forall m n (M : 'M[R]_(m,n)) (X : 'rV_m), reflect (exists Y, X = Y *m ker_c M) (X *m M == 0).
proof: Proof. move=> m n; elim: n m=> [n m X | n ih m]. by rewrite ?thinmx0; apply: (iffP idP)=> //= _; exists X; rewrite mulmx1. rewrite [n.+1]/(1 + n)%nat => M /=; set G1 := ker_col (lsubmx M). move: (ih _ (G1 *m rsubmx M))=> {}ih X. apply: (iffP eqP)=> [|[Y hY]]; rewrite -{1}[M]hsubmxK (@mul_mx_row _ _ _ 1) -(@row_mx0 _ _ 1). case/(@eq_row_mx _ _ 1); case/eqP/ker_colP=> V ->; rewrite -mulmxA. by case/eqP/ih=> W ->; exists W; rewrite mulmxA. f_equal; apply/eqP. by apply/ker_colP; exists (Y *m ker_c (G1 *m rsubmx M)); rewrite -mulmxA. by rewrite hY mulmxA -[_ *m rsubmx M]mulmxA; apply/ih; exists Y. 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