proposition: Lemma mulmx_ebase m n (M : 'M_(m, n)) : col_ebase M *m diag_mx M *m row_ebase M = M.
proof: Proof. rewrite /col_ebase /diag_mx /row_ebase /diag /smith_seq. case: smithP => /= L0 d R0 h1 h2 L0unit R0unit. rewrite diag_mx_seq_filter0 ?(sorted_take (@dvdr_trans [the dvdRingType of R])) // diag_mx_seq_take_min. by rewrite -h1 !mulmxA mulVmx // mul1mx -mulmxA mulmxV ?mulmx1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path tuple) mathcomp(perm fingroup choice ssralg fintype finfun poly polydiv) mathcomp(bigop matrix zmodp mxalgebra) ssrcomplements dvdring mxstructure similar minor binetcauchy stronglydiscrete coherent