proposition: Lemma refine_Madd_mnm_add {n} (m : 'X_{1.. n}) m' (c : T) p p' : refines Rseqmultinom m m' -> refines Reffmpoly p p' -> m \notin msupp p -> refines Reffmpoly (+%R (c *: 'X_[m]) p) (M.add m' c p').
proof: Proof. move=> Hm Hp Hnotin. apply: refine_effmpolyP. { move=> k /F.add_in_iff [Hk|Hk]. - move/mnmc_eq_seqP/eqP: Hk <-. apply RseqmultinomE in Hm. by rewrite -(size_map spec_N m') -Hm size_tuple. - by apply (@refine_size_mpoly _ _ _ _ Hp). } move=> l l' Hl; rewrite mcoeffD mcoeffZ mcoeffX. case: (boolP (m == l)) => Heq /=. { rewrite mulr1. rewrite F.add_eq_o /=; last first. { apply/mnmc_eq_seqP. apply RseqmultinomE in Hm. apply RseqmultinomE in Hl. move/eqP/(congr1 (@tval n nat \o val)) in Heq. rewrite /= Hm Hl in Heq. exact/eqP/map_spec_N_inj. } move/eqP in Heq; rewrite Heq in Hnotin. by rewrite memN_msupp_eq0 // addr0. } rewrite mulr0 add0r. rewrite F.add_neq_o /=; last first. { apply/mnmc_eq_seqP. apply/negbT; rewrite -(@Rseqmultinom_eq _ _ _ _ _ Hm Hl). by move/negbTE: Heq ->. } rewrite refinesE in Hp. exact: refine_find_mpoly. 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)