proposition: Lemma freeg_sumE D : \sum_(z <- dom D) << (coeff z D) *g z >> = D.
proof: Proof. apply/eqP/freeg_eqP=> x /=; rewrite raddf_sum /=. case x_in_dom: (x \in dom D); last rewrite coeff_outdom ?x_in_dom //. + rewrite (bigD1_seq x) ?uniq_dom //= big1 ?addr0. * by rewrite coeffU eqxx mulr1. * by move=> z ne_z_x; rewrite coeffU (negbTE ne_z_x) mulr0. + rewrite big_seq big1 // => z z_notin_dom; rewrite coeffU. have ->: (z == x)%:R = 0 :> R; last by rewrite mulr0. by case: (z =P x)=> //= eq_zx; rewrite eq_zx x_in_dom in z_notin_dom. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)