proposition: Lemma smithmxnP : forall m n (M : 'M[R]_(m,n)), smith_spec M (smithmxn smith2x2 M).
proof: Proof. case=> [|[[|[|n M]]|m [|[M|n M]]]] /=; do ?by constructor; rewrite ?unitmx1 ?flatmx0 ?thinmx0 ?diag_mx_seq_nil. - constructor; rewrite ?unitmx1 // mul1mx mulmx1. by apply/rowP=> i; rewrite ord1 !mxE. - exact: (smith1xnP _ (@smith2xnP _)). - case: (smith1xnP _ (@smith2xnP _))=> L1 d R1 h1 h2 h3 h4. constructor; rewrite ?unitmx_tr //. by apply/trmx_inj; rewrite !trmx_mul !trmxK tr_diag_mx_seq mulmxA. exact: smithmxn_recP. Qed.
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