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