proposition: Lemma eq_rank_unitmx m1 m2 n (U : 'M_(m1, n)) (V : 'M_(m2, n)) : \rank U = \rank V -> {f : 'M_n | f \in unitmx & V :=: U *m f}%MS.
proof: Proof. move=> eqrUV; pose f := invmx (row_ebase <<U>>%MS) *m row_ebase <<V>>%MS. have defUf: (<<U>> *m f :=: <<V>>)%MS. rewrite -[<<U>>%MS]mulmx_ebase mulmxA mulmxK ?row_ebase_unit // -mulmxA. rewrite genmxE eqrUV -genmxE -{3}[<<V>>%MS]mulmx_ebase -mulmxA. move: (pid_mx _ *m _) => W; apply/eqmxP. by rewrite !eqmxMfull ?andbb // row_full_unit col_ebase_unit. have{defUf} defV: (V :=: U *m f)%MS. by apply/eqmxP; rewrite -!(eqmxMr f (genmxE U)) !defUf !genmxE andbb. have injfU: \rank (U *m f) = \rank U by rewrite -defV eqrUV. by have [g injg defUg] := complete_unitmx injfU; exists g; rewrite -?defUg. 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)