proposition: Lemma deg1pos (D : {freeg K}) : 0 <=g D -> deg D = 1 -> exists x, D = << x >>.
proof: Proof. move=> D_ge0 degD_eq1; have: D != 0. by case: (D =P 0) degD_eq1 => [->|//]; rewrite deg0. rewrite -dom_eq0; case DE: (dom D) => [//|p ps] _. rewrite -[D]addr0 -(subrr <<p>>) addrA addrAC. have: coeff p D != 0. by move: (mem_dom D p); rewrite DE in_cons eqxx. rewrite neq_lt ltNge; have/fgposP/(_ p) := D_ge0 => ->/=. move=> coeffpD_gt0; have: 0 <=g (D - <<p>>). apply/fgposP=> q; rewrite coeffB coeffU mul1r. case: (p =P q) =>[<-/=|]; last first. by move=> _; rewrite subr0; apply/fgposP. by rewrite subr_ge0. move/fgpos_eq0P=> ->; first by rewrite add0r; exists p. by rewrite degB degU degD_eq1 subrr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)