proposition: Lemma size_Smith m n (A : 'M_(m,n)) : let: (_, d, _) := Smith A in (size d <= minn m n)%N.
proof: Proof. elim: m n A=>[n'|m' Ih n']; first by rewrite min0n. case: n'=>[|n' A /=]; first by rewrite minn0. case: find_pivotP=> [[x1 x2] Hx|//]. case: (improve_pivot _ _); case => a b c /=; set M := map_mx _ _. case H: (Smith _) (Ih n' M) => [[i s] k] /=. by rewrite size_map minnSS ltnS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg ssrint ssrnum fintype choice) mathcomp(matrix mxalgebra bigop zmodp perm) dvdring mxstructure stronglydiscrete coherent edr