proposition: Lemma freeg_rect_dom D: P D.
proof: Proof. rewrite -[D]freeg_sumE (bigID F) /=; set DR := \sum_(_ <- _ | _) _. have: [predI dom DR & [predC F]] =1 pred0. move=> p /=; rewrite !inE; apply/negP=> /andP []. rewrite /DR => /dom_sum_subset /flattenP. case=> [ps /mapP [q]]; rewrite mem_filter => /andP []. move=> Rq q_in_D ->; rewrite domU ?mem_seq1; last first. by rewrite -(mem_dom D q). by move/eqP=> ->; move: Rq; rewrite /in_mem /= => ->. move: DR => DR domDR; rewrite addrC -big_filter. set ps := [seq _ <- _ | _]; move: (perm_refl ps). rewrite {1}/ps; move: ps (D) => {D}; elim => [|p ps IH] D. + by move=> _; rewrite big_nil add0r; apply: H0. + move=> DE; move: (perm_mem DE p); rewrite !inE eqxx /=. have /=: uniq (p :: ps). by move/perm_uniq: DE; rewrite filter_uniq // uniq_dom. case/andP=> p_notin_ps uniq_ps; rewrite mem_filter=> /andP [NRp p_in_D]. rewrite big_cons -addrA; apply: HS => //; first 1 last. * by move: p_in_D; rewrite mem_dom. * pose D' := D - << coeff p D *g p >>. have coeffD' q: coeff q D' = coeff q D * (p != q)%:R. rewrite {}/D' coeffB coeffU; case: (p =P q). - by move=> ->; rewrite !(mulr1, mulr0) subrr. - by move/eqP=> ne_pq; rewrite !(mulr1, mulr0) subr0. have: perm_eq (dom D) (p :: dom D'). apply: uniq_perm; rewrite /= ?uniq_dom ?andbT //. - by rewrite mem_dom coeffD' eqxx mulr0 eqxx. move=> q; rewrite in_cons !mem_dom coeffD' [q == _]eq_sym. case: (p =P q); rewrite !(mulr0, mulr1) //=. by move=> <-; move: p_in_D; rewrite mem_dom. move/perm_filter=> /(_ [pred q | ~~ (F q)]) /=. rewrite NRp; rewrite perm_sym; move/perm_trans => /(_ _ DE). rewrite perm_cons => domD'; rewrite big_seq. rewrite (eq_bigr (fun q => << coeff q D' *g q >>)); last first. move=> q q_in_ps; rewrite /D' coeffB coeffU; case: (p =P q). - by move=> eq_pq; move: p_notin_ps; rewrite eq_pq q_in_ps. - by move=> _; rewrite mulr0 subr0. by rewrite -big_seq; apply: IH. * apply/negP=> /domD_subset; rewrite mem_cat; case/orP; last first. by move=> p_in_DR; move/(_ p): domDR; rewrite !inE NRp p_in_DR. move/dom_sum_subset; rewrite filter_predT => /flattenP [qs]. move/mapP => [q q_in_ps ->]; rewrite domU; last first. move/perm_mem/(_ q): DE; rewrite !inE q_in_ps orbT. by rewrite mem_filter => /andP [_]; rewrite mem_dom. rewrite mem_seq1 => /eqP pq_eq; move: p_notin_ps. by rewrite pq_eq q_in_ps. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)