proposition: Lemma equiv_diag_block : forall l1 l2, size l1 = size l2 -> forall (F1 F2 : forall n : nat, nat -> 'M_n.+1), (forall i, i < size l1-> equivalent (F1 (nth 0%N l1 i) i) (F2 (nth 0%N l2 i) i)) -> equivalent (diag_block_mx l1 F1) (diag_block_mx l2 F2).
proof: Proof. case=>[|a l1]; case=> //=. by move=> *; exact: equiv_refl. move=> b l2 /eqP; rewrite eqSS=> /eqP Hsl F1 F2 Hl. have Hab: equivalent (F1 a 0%N) (F2 b 0%N) by exact: (Hl 0%N). move: l1 l2 Hsl a b F1 F2 Hab Hl. apply: seq2_ind=> //= x1 x2 l1 l2 IH a b F1 F2 Hab H. apply: (equiv_dgblockmx Hab). apply: IH=>[|i]; first exact: (H 1%N). exact: (H i.+1). 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