proposition: Lemma coeff_fgnegE D k : coeff k (fgneg D) = - Num.min 0 (coeff k D).
proof: Proof. by rewrite -fgposN coeff_fgposE coeffN -{1}[0]oppr0 -oppr_min. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)