proposition: Lemma deg1neg (D : {freeg K}) : D <=g 0 -> deg D = -1 -> exists x, D = - << x >>.
proof: Proof. move=> D_le0 degD_eqN1; case: (@deg1pos (-D)). + apply/fgleP=> p; rewrite coeffN coeff0 oppr_ge0. by move/fgleP/(_ p): D_le0; rewrite coeff0. + by rewrite degN degD_eqN1 opprK. + by move=> p /eqP; rewrite eqr_oppLR => /eqP->; exists p. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)