proposition: Lemma similar_diag_mx_seq m n s1 s2 : m = n -> size s1 = m -> perm_eq s1 s2 -> similar (diag_mx_seq m m s1) (diag_mx_seq n n s2).
proof: Proof. move=> eq Hms Hp. have Hs12:= perm_size Hp. have Hs2: size s2 == n by rewrite -Hs12 Hms eq. pose t:= Tuple Hs2. have HE: s2 = t by []. move: Hp; rewrite HE. case/tuple_permP=> p Hp. split=> //; rewrite eq. exists (perm_mx p)^T; first by rewrite unitmx_tr unitmx_perm. apply/matrixP=> i j; rewrite conform_mx_id !mxE (bigD1 j) //= big1 ?addr0. rewrite (bigD1 i) //= big1 ?addr0. rewrite !mxE Hp -tnth_nth tnth_mktuple (tnth_nth 0) HE !eqxx. case: (p j == i) /eqP => Hij; first by rewrite Hij mulr1 mul1r. by rewrite mulr0 mul0r. by move=> k /negbTE Hk; rewrite !mxE eq_sym (inj_eq (@ord_inj _)) Hk mul0r. by move=> k /negbTE Hk; rewrite !mxE (inj_eq (@ord_inj _)) Hk mulr0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype fintype finfun ssrnat seq) mathcomp(choice ssralg poly polydiv mxpoly matrix bigop) mathcomp(mxalgebra perm fingroup tuple) mxstructure dvdring