proposition: Lemma row_freeP m n (A : 'M_(m, n)) : reflect (exists B, A *m B = 1%:M) (row_free A).
proof: Proof. rewrite /row_free -mxrank_tr. apply: (iffP row_fullP) => [] [B kA]; by exists B^T; rewrite -trmx1 -kA 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)