proposition: Lemma mulmx1_min m n (A : 'M[R]_(m, n)) B : A *m B = 1%:M -> m <= n.
proof: Proof. move=> AB1; rewrite leqNgt; apply/negP=> /subnKC; rewrite addSnnS. move: (_ - _)%N => m' def_m; move: AB1; rewrite -{m}def_m in A B *. rewrite -(vsubmxK A) -(hsubmxK B) mul_col_row scalar_mx_block. case/eq_block_mx=> /mulmx1C BlAu1 AuBr0 _ => /eqP/idPn[]. by rewrite -[_ B]mul1mx -BlAu1 -mulmxA AuBr0 !mulmx0 eq_sym oner_neq0. 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 countalg finalg zmodp)