proposition: Lemma trigsqmx_ind (P : forall n, 'M[V]_n -> Type) : (P 0 0) -> (forall n x c A, is_trig_mx A -> P n A -> P (1 + n)%N (block_mx x 0 c A)) -> forall n A, is_trig_mx A -> P n A.
proof: Proof. move=> P0 PS n A; elim/sqmx_ind: A => {n} [|n x r c] A PA. by rewrite thinmx0; apply: P0. 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)