proposition: Lemma row_ind m (P : forall n, 'M[R]_(m, n) -> Type) : (forall A, P 0 A) -> (forall n c A, P n A -> P (1 + n)%N (row_mx c A)) -> forall n A, P n A.
proof: Proof. move=> P0 PS; elim=> [//|n IHn] A. by rewrite -[n.+1]/(1 + n)%N in A *; rewrite -[A]hsubmxK; 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)