proposition: Lemma row_full_inj m n p A : row_full A -> injective (@mulmx F m n p A).
proof: Proof. case/row_fullP=> A' A'K; apply: can_inj (mulmx A') _ => B. by rewrite mulmxA A'K mul1mx. 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)