proposition: Lemma rank_leq_row m n (A : 'M_(m, n)) : \rank A <= m.
proof: Proof. rewrite mxrankE. elim: m n A => [|m IHm] [|n] //= A; case: pickP => [[i j] _|] //=. by move: (_ - _) => B; case: GaussE (IHm _ B) => [[L U] r] /=. 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)