proposition: Lemma ext_block s (F1 F2 : forall n, nat -> 'M_n.+1) : (forall i, i < size s -> (F1 (nth 0%N s i) i) = (F2 (nth 0%N s i) i)) -> diag_block_mx s F1 = diag_block_mx s F2.
proof: Proof. case: s=> // a l. elim: l a F1 F2=> /= [a F1 F2 Hi|b l IHl a F1 F2 Hi]. exact: (Hi 0%N). set F3 := (fun n i : nat => _). set F4 := (fun n i : nat => _). rewrite (Hi 0%N) // (IHl b F3 F4) //. by move=> i Hi2; apply: (Hi i.+1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm poly mxpoly finfun tuple) mathcomp(matrix bigop zmodp polydiv) ssrcomplements dvdring