proposition: Lemma mxrank_delta m n i j : \rank (delta_mx i j : 'M_(m, n)) = 1.
proof: Proof. apply/eqP; rewrite eqn_leq lt0n mxrank_eq0. rewrite -{1}(mul_delta_mx (0 : 'I_1)) mulmx_max_rank. by apply/eqP; move/matrixP; move/(_ i j); move/eqP; rewrite !mxE !eqxx oner_eq0. 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)