proposition: Lemma refine_Madd_mnm_add_sum n m m' c (p : mpoly n T) p' : refines Rseqmultinom m m' -> refines (Reffmpoly (T := T) (n := n)) p p' -> refines Reffmpoly (\sum_(i2 <- msupp p) (c * p@_i2) *: 'X_[m + i2]) (M.fold (fun (l' : M.key) (c' : T) => M.add (mnm_add_seq m' l') (c * c')%C) p' M.empty).
proof: Proof. move=> ref_m; move: p. apply P.fold_rec. { move=> q' Eq' q Hq. match goal with | [ |- refines Reffmpoly ?pol M.empty ] => suff ->: pol = 0 end. { by apply refine_mp0_eff. } apply /mpolyP => l. rewrite big1 ?mcoeff0 //. move=> i _. rewrite (refine_find_mpoly Hq (refine_seqmultinom_of_multinom i)) /=. case_eq (M.find (seqmultinom_of_multinom i) q') =>[s|/=]. - rewrite -F.find_mapsto_iff F.elements_mapsto_iff. by rewrite -in_InA_eq_key_elt_iff (proj1 (P.elements_Empty _ ) Eq'). - by move=> _; rewrite mulr0 scale0r. } move=> k' e q p'' p''' Hmap Hin Hadd Hind p ref_p. pose k := multinom_of_seqmultinom_val n k'. have Hk : refines Rseqmultinom k k'; [by apply (refine_size_add Hadd ref_p)|]. have Hp : p@_k = e. { rewrite (refine_find_mpoly ref_p Hk) Hadd F.add_eq_o //. exact: E.eq_refl. } pose p0 := (c * e) *: 'X_[m + k]. pose pmpk := p - p@_k *: 'X_[k]. have Hpmpk : pmpk@_k = 0. { by rewrite mcoeffB mcoeffZ mcoeffX eqxx Hp mulr1 subrr. } set sum := \sum_(_ <- _) _. have->: sum = p0 + \big[+%R/0]_(i2 <- msupp pmpk) ((c * pmpk@_i2) *: 'X_[(m + i2)]). { rewrite /sum /pmpk /p0. case_eq (k \in msupp p) => Hmsuppp. { rewrite (big_rem _ Hmsuppp) /= Hp; f_equal. rewrite -Hp -(perm_big _ (msupp_rem p k)) /=. apply eq_big_seq => i. rewrite mcoeffB mcoeffZ mcoeffX. rewrite mcoeff_msupp Hp -Hpmpk. case (boolP (k == i)). { move/eqP<-; rewrite Hpmpk. by rewrite mcoeffB Hp mcoeffZ mcoeffX eqxx mulr1 subrr eqxx. } by rewrite mulr0 subr0. } move: Hmsuppp; rewrite mcoeff_msupp Hp; move/eqP ->. by rewrite mulr0 !scale0r add0r subr0. } rewrite /p0. apply refine_Madd_mnm_add. { eapply refines_apply; first by eapply refines_apply; tc. rewrite /k. apply refine_multinom_of_seqmultinom_val. apply (@refine_size_mpoly _ _ _ _ ref_p). red in Hadd. apply/F.in_find_iff. rewrite Hadd F.add_eq_o //. exact/mnmc_eq_seqP. } { eapply Hind. apply (rem_mpoly_eff Hin Hadd ref_p Hk). } rewrite mcoeff_msupp negbK. set F' := fun i2 => (c *: 'X_[m]) * (pmpk@_i2 *: 'X_[i2]). rewrite (eq_bigr F'). { rewrite -big_distrr /= -mpolyE. rewrite (mcoeff_poly_mul _ _ (k:=(mdeg (m + k)).+1)) //. rewrite big1 // => k0. case (boolP (m == k0.1)). { by move/eqP<-; rewrite eqm_add2l; move/eqP <-; rewrite Hpmpk mulr0. } by rewrite mcoeffZ mcoeffX; move /negbTE ->; rewrite mulr0 mul0r. } move=> m'' _; rewrite /F'; rewrite mpolyXD. rewrite -scalerAl -scalerA; f_equal. by rewrite -[RHS]commr_mpolyX -scalerAl commr_mpolyX. Qed.
imports: ZArith NArith FMaps FMapAVL mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice finfun tuple fintype ssralg bigop) CoqEAL(hrel) CoqEAL(refinements) CoqEAL(param binord binnat) CoqEAL(seqmx ) CoqEAL(ssrcomplements) mathcomp.multinomials(mpoly freeg)