proposition: Lemma fg_decomp D : D = fgpos D - fgneg D.
proof: Proof. apply/eqP/freeg_eqP=> k; rewrite coeffB. by rewrite coeff_fgposE coeff_fgnegE opprK addr_max_min add0r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)