proposition: Lemma mdeg_eq1 m : (mdeg m == 1%N) = [exists i : 'I_n, m == U_(i)%MM].
proof: Proof. apply/eqP/idP=> [|/existsP[i /eqP ->]]; last by rewrite mdeg1. rewrite [m]multinomUE_id => Hmdeg. have: [exists i, m i != 0%N]. rewrite -negb_forall; apply/contra_eqN: Hmdeg => /forallP Hm0. by rewrite big1 ?mdeg0 //= => i _; rewrite (eqP (Hm0 i)). case/existsP => i Hi; apply/existsP; exists i; move: Hmdeg. rewrite (bigD1 i) //= mdegD mdegMn mdeg1 mul1n. case: (m i) Hi => [|[|]] //= _ [] /eqP; rewrite mdeg_eq0 => /eqP ->. by rewrite mulm1n addm0. 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