fact: Definition smithmxn m n : 'M[R]_(m,n) -> 'M[R]_m * seq R * 'M[R]_n := match m,n with | 0,_ => fun _ => (1%:M,[::],1%:M) | _,0 => fun _ => (1%:M,[::],1%:M) | 1,1 => fun A => (1%:M,[:: A 0 0],1%:M) | 1,_.+2 => smith1xn (@smith2xn _) | _.+2,1 => fun A => let: (L,d,R) := smith1xn (@smith2xn _) A^T in (R^T,d,L^T) | _.+2,_.+2 => fun A => smithmxn_rec A end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype matrix mxalgebra bigop zmodp perm choice) dvdring mxstructure minor stronglydiscrete coherent edr