proposition: Lemma lep1mP i m : (U_(i) <= m)%MM = (m i != 0%N).
proof: Proof. apply/mnm_lepP/idP=> [/(_ i)|]; rewrite -lt0n; first by rewrite mnm1E eqxx. by move=> lt0_mi j; rewrite mnm1E; case: eqP=> // <-. 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