proposition: Lemma trigmx_ind (P : forall m n, 'M_(m, n) -> Type) : (forall m, P m 0 0) -> (forall n, P 0 n 0) -> (forall m n x c A, is_trig_mx A -> P m n A -> P (1 + m)%N (1 + n)%N (block_mx x 0 c A)) -> forall m n A, is_trig_mx A -> P m n A.
proof: Proof. move=> P0l P0r PS m n A; elim: A => {m n} [m|n|m n xx r c] A PA; do ?by rewrite (flatmx0, thinmx0); by [apply: P0l|apply: P0r]. by rewrite is_trig_block_mx => // /and3P[/eqP-> _ Atrig]; apply: PS (PA _). 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)