proposition: Lemma coeff_fgposE D k : coeff k (fgpos D) = Num.max 0 (coeff k D).
proof: Proof. by rewrite fgmap_f0_coeffE ?normr0 //=; case: ger0P. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)