proposition: Lemma sqmx_ind (P : forall n, 'M[R]_n -> Type) : (forall A, P 0 A) -> (forall n x r c A, P n A -> P (1 + n)%N (block_mx x r c A)) -> forall n A, P n A.
proof: Proof. by move=> P0 PS; elim=> [//|n IHn] A; rewrite -[A](@submxK 1 _ 1); apply: PS. 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)