proposition: Lemma is_trig_mxblockP (B_ : forall i j, 'M[V]_(p_ i, p_ j)) : reflect [/\ forall (i j : 'I_p), (i < j)%N -> B_ i j = 0 & forall i, is_trig_mx (B_ i i)] (is_trig_mx (\mxblock_(i, j) B_ i j)).
proof: Proof. apply: (iffP is_trig_mxP); last first. move=> [Blt1 /(_ _)/is_trig_mxP Blt2]/= s s'; rewrite !mxE. rewrite -[_ < _]lt_sig ltEsig/= /sig1 /sig2 leEord. case: ltngtP => //= ii'; first by rewrite (Blt1 _ _ ii') mxE. move: (sig s) (sig s') ii' => -[/= i j] [/= i' +] /val_inj ii'. by case: _ / ii' => j'; rewrite tagged_asE => /Blt2->. move=> Btrig; split=> [i i' lti|i]. apply/matrixP => j j'; have := Btrig (Rank _ j) (Rank _ j'). rewrite !mxE !Rank2K; do !case: _ / esym; rewrite !cast_ord_id. rewrite /Rank [_ <= _]lt_rank. by rewrite ltEsig/= leEord ltnW//= (ltn_geF lti)//= => /(_ isT). apply/is_trig_mxP => j j' ltj; have := Btrig (Rank _ j) (Rank _ j'). rewrite !mxE !Rank2K; do! case: _ / esym; rewrite !cast_ord_id. by rewrite [_ <= _]lt_rank ltEsig/= !leEord leqnn/= tagged_asE; 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)