proposition: Lemma eqd_equiv n m n' m' (s1 s2 : seq R) : n = n' -> m = m' -> size s1 = size s2 -> (forall i, nth 0 s1 i %= nth 0 s2 i) -> equivalent (diag_mx_seq n m s1) (diag_mx_seq n' m' s2).
proof: Proof. move=> <- <-. case: n=> [_ _|n]; first exact: equiv0l. case: m=> [_ _|m Hs]; first exact: equiv0r. move: Hs n m. pose P := (fun (s1 s2 : seq R) => forall n m, (forall i, nth 0 s1 i %= nth 0 s2 i) -> equivalent (diag_mx_seq n.+1 m.+1 s1) (diag_mx_seq n.+1 m.+1 s2)). apply: (seq2_ind (P:=P))=> /= [n m _ | x1 x2 s0 s3 IH n m Hi]. by rewrite !diag_mx_seq_nil; apply: equiv_refl. rewrite /P !diag_mx_seq_cons. have IHi: (forall i : nat, s0`_i %= s3`_i). by move=> i; move: (Hi i.+1); rewrite -nth_behead. have Hxp : x1 %= x2 by move: (Hi 0%N); rewrite nth0. have Hx12: (@equivalent _ 1 1 1 1 x1%:M x2%:M). split=> //; case/eqdP: Hxp=> c Hc Hcx. rewrite conform_mx_id. exists c%:M; exists 1%:M; split. + by rewrite -scalemx1 unitmxZ // unitmx1. + by rewrite unitmx1. by rewrite mul_scalar_mx scale_scalar_mx mulmx1 Hcx. apply: (equiv_dgblockmx Hx12). case: n=> [|n]; first exact: equiv0l. case: m=> [|m]; first exact: equiv0r. exact: (IH n m IHi). 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