proposition: Lemma mx_ind (P : forall m n, 'M[R]_(m, n) -> Type) : (forall m A, P m 0 A) -> (forall n A, P 0 n A) -> (forall m n x r c A, P m n A -> P (1 + m)%N (1 + n)%N (block_mx x r c A)) -> forall m n A, P m n A.
proof: Proof. move=> P0l P0r PS; elim=> [|m IHm] [|n] A; do ?by [apply: P0l|apply: P0r]. by 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)