proposition: Lemma complete_unitmx m n (U : 'M_(m, n)) (f : 'M_n) : \rank (U *m f) = \rank U -> {g : 'M_n | g \in unitmx & U *m f = U *m g}.
proof: Proof. move=> injfU; pose V := <<U>>%MS; pose W := V *m f. pose g := proj_mx V (V^C)%MS *m f + cokermx V *m row_ebase W. have defW: V *m g = W. rewrite mulmxDr mulmxA proj_mx_id ?genmxE ?capmx_compl //. by rewrite mulmxA mulmx_coker mul0mx addr0. exists g; last first. have /submxP[u ->]: (U <= V)%MS by rewrite genmxE. by rewrite -!mulmxA defW. rewrite -row_full_unit -sub1mx; apply/submxP. have: (invmx (col_ebase W) *m W <= V *m g)%MS by rewrite defW submxMl. case/submxP=> v def_v; exists (invmx (row_ebase W) *m (v *m V + (V^C)%MS)). rewrite -mulmxA mulmxDl -mulmxA -def_v -{3}[W]mulmx_ebase -mulmxA. rewrite mulKmx ?col_ebase_unit // [_ *m g]mulmxDr mulmxA. rewrite (proj_mx_0 (capmx_compl _)) // mul0mx add0r 2!mulmxA. rewrite mulmxK ?row_ebase_unit // copid_mx_id ?rank_leq_row //. rewrite (eqmxMr _ (genmxE U)) injfU genmxE addrC -mulmxDl subrK. by rewrite mul1mx mulVmx ?row_ebase_unit. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)