proposition: Lemma ltmwf : (forall m1, (forall m2, (m2 < m1)%O -> P m2) -> P m1) -> forall m, P m.
proof: Proof. pose tof m := [tuple of mdeg m :: m]. move=> ih m; move: {2}(tof _) (erefl (tof m))=> t. elim/(@ltxwf _ nat): t m=> //=; last first. move=> t wih m Em; apply/ih=> m' lt_m'm. by apply/(wih (tof m')); rewrite // -Em. move=> Q {}ih x; elim: x {-2}x (leqnn x). move=> x; rewrite leqn0=> /eqP->; apply/ih. by move=> y; rewrite ltEnat/= ltn0. move=> k wih l le_l_Sk; apply/ih=> y; rewrite ltEnat => lt_yl. by apply/wih; have := leq_trans lt_yl le_l_Sk; rewrite ltnS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg