proposition: Lemma is_trig_mxblock (B_ : forall i j, 'M[V]_(p_ i, p_ j)) : is_trig_mx (\mxblock_(i, j) B_ i j) = ([forall i : 'I_p, forall j : 'I_p, (i < j)%N ==> (B_ i j == 0)] && [forall i, is_trig_mx (B_ i i)]).
proof: Proof. by apply/is_trig_mxblockP/andP => -[] => [/(_ _ _ _)/eqP|] => /'forall_'forall_implyP => [|/(_ _ _ _)/eqP] Blt /forallP. 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)