proposition: Lemma size_Smith m n (M : 'M_(m,n)) : let: (_, d, _) := Smith M in (size d <= minn m n)%N.
proof: Proof. elim: m n M => [n'|m' Ih n']; first by rewrite min0n. case: n' => [|n' M /=]; first by rewrite minn0. case: find_pivotP=> [[x1 x2] Hx|//]. case: (improve_pivot _); case => a b c /=. case H: (Smith _)=>[[i j] k]. rewrite /= size_map minnSS ltnS. move: (Ih n' (map_mx (fun x => odflt 0 (x %/? b 0 0)) (drsubmx b - const_mx 1 *m ursubmx b))). by rewrite H. 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