proposition: Lemma ker_c_intP : forall m (V : 'cV_m) (X : 'rV_m), reflect (exists Y, X = Y *m ker_c_int V) (X *m V == 0).
proof: Proof. elim => [V X | n IH] /=. rewrite thinmx0 flatmx0 /ker_c_int mulmx0 eqxx. by constructor; exists 0; rewrite mulmx0. rewrite [n.+1]/(1 + n)%nat => V X. set v := usubmx V. set vs := dsubmx V. set x := lsubmx X. set xs := rsubmx X. set m0 := ker_c_int vs. set wv := cap_wl v (-vs). set wvs := cap_wr v (-vs). move: (wl v (-vs)); rewrite -/wv => Hwv. move: (wr v (-vs)); rewrite -/wvs => Hwvs. rewrite -[V]vsubmxK -[X]hsubmxK. case: (eqVneq v 0) => v0. apply: (iffP idP) => /= [|[W ->]]. rewrite (@mul_row_col _ _ 1) -/v v0 mulmx0 add0r => vs0. case: (IH vs xs) => [[A HA]|[]]; last by apply/IH. exists (row_mx (const_mx (x 0 0)) A). rewrite (@mul_row_block _ _ _ _ 1) -/xs !mulmx0 add0r addr0 -colE col_const HA. by f_equal; apply/rowP => i; rewrite !mxE /= !ord1. rewrite -mulmxA (@mul_block_col _ _ _ 1) -/v !mul0mx addr0 add0r. rewrite -[W]hsubmxK mul_row_col {6}v0 !mulmx0 add0r mulmxA. by apply/IH; exists (rsubmx W). apply: (iffP idP) => /= [|[W ->]]. rewrite (@mul_row_col _ _ 1) => hwx. have vx00 : ((x * v) 0 0)%:M = x * v. by apply/matrixP=> i j; rewrite !ord1 !mxE eqxx. have : member ((x * v) 0 0) (cap v (- vs)). case: cap_spec => c /= _ _ in_int. apply: in_int; first by apply/memberP; exists x; rewrite vx00. apply/memberP; exists xs; apply/eqP. move: hwx; rewrite -/v -/vs -/x -/xs mulmxN addr_eq0 => /eqP <-. by rewrite vx00. case/memberP=> W hW. case: (IH vs (xs - (W *m wvs))) => [[A HA]|[]]. exists (row_mx W A). rewrite (@mul_row_block _ _ _ _ 1) mulmx0 addr0 -HA addrCA subrr addr0. f_equal; apply/(@scalemx_inj _ _ _ (v 0 0)). apply: contra_neq v0 => v00. by apply/rowP => i; rewrite !ord1 /= v00 !mxE. by rewrite -!mul_mx_scalar -mx11_scalar -mulmxA Hwv -hW -/x vx00. by apply/IH; rewrite mulmxDl mulNmx addrC -mulmxN -mulmxA Hwvs -hW vx00. rewrite -[W]hsubmxK (@mul_row_block _ _ _ _ 1) mulmx0 addr0 (@mul_row_col _ _ 1). rewrite -!mulmxA Hwv addr_eq0 -mulmxN mulmxDl -!mulmxA Hwvs addrC -subr_eq. rewrite addrN -/vs !mulmxN eq_sym oppr_eq0 mulmxA. case: (IH vs _) => // [[]]. by exists (rsubmx W). 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