proposition: Lemma eqmxMunitP m n (U V : 'M_(m, n)) : reflect (exists2 P, P \in unitmx & U = P *m V) (U == V)%MS.
proof: Proof. apply: (iffP eqmxP) => [eqUV | [P Punit ->]]; last first. by apply/eqmxMfull; rewrite row_full_unit. have [D defU]: exists D, U = D *m V by apply/submxP; rewrite eqUV. have{eqUV} [Pt Pt_unit defUt]: {Pt | Pt \in unitmx & V^T *m D^T = V^T *m Pt}. by apply/complete_unitmx; rewrite -trmx_mul -defU !mxrank_tr eqUV. by exists Pt^T; last apply/trmx_inj; rewrite ?unitmx_tr // defU !trmx_mul trmxK. 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)