proposition: Lemma rem_mpoly_eff n (q p' : effmpoly T) (k' : seqmultinom) (e : T) (p : mpoly n T) (k : 'X_{1..n}) : ~ M.In k' q -> P.Add k' e q p' -> refines Reffmpoly p p' -> refines Rseqmultinom k k' -> refines Reffmpoly (p - p@_k *: 'X_[k]) q.
proof: Proof. move=> Hin Hadd Hp Hk. apply refine_effmpolyP. { move=> m'' [c' Hc']; move: (Hadd m''); rewrite F.add_o. case E.eq_dec. { move/mnmc_eq_seqP/eqP <-; rewrite -F.find_mapsto_iff => Hm. by apply (@refine_size_mpoly _ _ _ _ (Hp)); exists e. } rewrite (proj1 (F.find_mapsto_iff q m'' c')) // => _ H. apply (@refine_size_mpoly _ _ _ _ (Hp)). by exists c'; move: H; rewrite -F.find_mapsto_iff. } move=> mm mm' ref_mm; move: (Hadd mm'); rewrite F.add_o. rewrite mcoeffB mcoeffZ mcoeffX. case E.eq_dec. { move/mnmc_eq_seqP/eqP => Hmm'; rewrite -Hmm'. have Hmm : k = mm. { by apply/eqP; rewrite (Rseqmultinom_eq Hk ref_mm); apply/eqP. } rewrite (proj1 (F.not_find_in_iff _ _) Hin) -Hmm eqxx mulr1. by rewrite (refine_find_mpoly Hp Hk) => ->; rewrite subrr. } move=> Hmm' <-. have Hmm : ~ k = mm. { move=> Hmmm; apply/Hmm'/mnmc_eq_seqP. by rewrite -(Rseqmultinom_eq Hk ref_mm); apply/eqP. } rewrite (refine_find_mpoly Hp ref_mm). by have ->: (k == mm = false); [apply/eqP|rewrite mulr0 subr0]. 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)