proposition: Lemma is_trig_block_mx m1 m2 n1 n2 ul ur dl dr : m1 = n1 -> @is_trig_mx (m1 + m2) (n1 + n2) (block_mx ul ur dl dr) = [&& ur == 0, is_trig_mx ul & is_trig_mx dr].
proof: Proof. move=> eq_m1_n1; rewrite {}eq_m1_n1 in ul ur dl dr *. apply/is_trig_mxP/and3P => [Atrig|]; last first. move=> [/eqP-> /is_trig_mxP ul_trig /is_trig_mxP dr_trig] i j; rewrite !mxE. do 2![case: split_ordP => ? ->; rewrite ?mxE//=] => lt_ij; rewrite ?ul_trig//. move: lt_ij; rewrite ltnNge -ltnS. by rewrite (leq_trans (ltn_ord _))// -addnS leq_addr. by rewrite dr_trig//; move: lt_ij; rewrite ltn_add2l. split. - apply/eqP/matrixP => i j; have := Atrig (lshift _ i) (rshift _ j). rewrite !mxE; case: split_ordP => k /eqP; rewrite eq_shift// ?mxE. case: split_ordP => l /eqP; rewrite eq_shift// ?mxE => /eqP-> /eqP<- <- //. by rewrite /= (leq_trans (ltn_ord _)) ?leq_addr. - apply/is_trig_mxP => i j lt_ij; have := Atrig (lshift _ i) (lshift _ j). rewrite !mxE; case: split_ordP => k /eqP; rewrite eq_shift// ?mxE. by case: split_ordP => l /eqP; rewrite eq_shift// ?mxE => /eqP<- /eqP<- ->. - apply/is_trig_mxP => i j lt_ij; have := Atrig (rshift _ i) (rshift _ j). rewrite !mxE; case: split_ordP => k /eqP; rewrite eq_shift// ?mxE. case: split_ordP => l /eqP; rewrite eq_shift// ?mxE => /eqP<- /eqP<- -> //. by rewrite /= ltn_add2l. 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)