proposition: Lemma fgpos_eq0P (D : {freeg K}) : 0 <=g D -> deg D = 0 -> D = 0.
proof: Proof. move=> posD; rewrite -{1}[D]freeg_sumE raddf_sum /=. rewrite (eq_bigr (fun z => coeff z D)); last first. by move=> i _; rewrite degU. move/eqP; rewrite psumr_eq0; last by move=> i _; apply/fgposP. move/allP=> zD; apply/eqP; apply/freeg_eqP=> z; rewrite coeff0. case z_in_D: (z \in dom D); last first. by rewrite coeff_outdom // z_in_D. exact/eqP/zD. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)