proposition: Lemma is_diag_mxblockP (B_ : forall i j, 'M[V]_(p_ i, p_ j)) : reflect [/\ forall (i j : 'I_p), i != j -> B_ i j = 0 & forall i, is_diag_mx (B_ i i)] (is_diag_mx (\mxblock_(i, j) B_ i j)).
proof: Proof. apply: (iffP is_diag_mxP); last first. move=> [Bneq1 /(_ _)/is_diag_mxP Bneq2]/= s s'; rewrite !mxE. rewrite val_eqE -(can_eq sigK) /sig1 /sig2. move: (sig s) (sig s') => -[/= i j] [/= i' j']. rewrite -tag_eqE/= /tag_eq/= negb_and. case: eqVneq => /= [ii'|/Bneq1->]; last by rewrite !mxE. by rewrite -ii' in j' *; rewrite tagged_asE => /Bneq2. move=> Bdiag; split=> [i i' Ni|i]. apply/matrixP => j j'; have := Bdiag (Rank _ j) (Rank _ j'). rewrite !mxE !Rank2K; do !case: _ / esym; rewrite !cast_ord_id. by rewrite eq_Rank negb_and Ni; apply. apply/is_diag_mxP => j j' Nj; have := Bdiag (Rank _ j) (Rank _ j'). rewrite !mxE !Rank2K; do! case: _ / esym; rewrite !cast_ord_id. by rewrite eq_Rank negb_and val_eqE Nj orbT; apply. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg countalg finalg zmodp)