proposition: Lemma mxsub_ind (weight : forall m n, 'M[R]_(m, n) -> nat) (sub : forall m n m' n', ('I_m' -> 'I_m) -> ('I_n' -> 'I_n) -> Prop) (P : forall m n, 'M[R]_(m, n) -> Type) : (forall m n (A : 'M[R]_(m, n)), (forall m' n' f g, weight m' n' (mxsub f g A) < weight m n A -> sub m n m' n' f g -> P m' n' (mxsub f g A)) -> P m n A) -> forall m n A, P m n A.
proof: Proof. move=> Psub m n A; have [k] := ubnP (weight m n A). elim: k => [//|k IHk] in m n A *. rewrite ltnS => lt_A_k; apply: Psub => m' n' f g lt_A'_A ?. by apply: IHk; apply: leq_trans lt_A_k. 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)