proposition: Lemma refine_effmpolyP (n : nat) T (p : mpoly n T) (p' : effmpoly T) : (forall m, M.In m p' -> size m == n)%N -> (forall m m', refines Rseqmultinom m m' -> p@_m = odflt 0 (M.find m' p')) -> refines Reffmpoly p p'.
proof: Proof. move=> eq_sz eq_monom. assert (Hsz : P.for_all (fun (k : M.key) (_ : T) => size k == n) p'). { rewrite /is_true (P.for_all_iff _) => k e Hke. { by apply eq_sz; exists e. } by move=> _ _ _; move: Hke; move/mnmc_eq_seqP/eqP ->. } rewrite refinesE /Reffmpoly /mpoly_of_effmpoly /ofun_hrel ifT //; f_equal. apply mpolyP => m. pose m' := seqmultinom_of_multinom m. have Hm' : refines Rseqmultinom m m'. by rewrite refinesE; apply seqmultinom_of_multinomK. rewrite (eq_monom _ _ Hm') mcoeff_MPoly coeff_Freeg. case_eq (M.find m' p') => [c|] Hc. { change c with ((c, m).1); change m with ((c, m).2). apply precoeff_mem_uniqE. { rewrite /predom -map_comp. rewrite (@eq_map _ _ _ ((multinom_of_seqmultinom_val n) \o fst)) //. rewrite map_comp map_inj_in_uniq. { apply NoDupA_eq_key_uniq_fst, M.elements_3w. } move=> x y Hx Hy; apply multinom_of_seqmultinom_val_inj. { move: Hx; move/mapP => [xe Hxe ->]. apply/eqP /eq_sz; exists xe.2; apply/(M.elements_2 (e:=xe.2)). by apply in_InA_eq_key_elt_iff; rewrite -surjective_pairing. } move: Hy; move/mapP => [ye Hye ->]. apply/eqP /eq_sz; exists ye.2; apply/(M.elements_2 (e:=ye.2)). by apply in_InA_eq_key_elt_iff; rewrite -surjective_pairing. } apply M.find_2, M.elements_1, in_InA_eq_key_elt_iff in Hc. apply/mapP; exists (m', c) => //=; f_equal. by rewrite /m' /multinom_of_seqmultinom_val seqmultinom_of_multinomK. } apply precoeff_outdom. rewrite /predom -map_comp. rewrite (@eq_map _ _ _ ((multinom_of_seqmultinom_val n) \o fst)) //. apply/negP=> Hm; apply F.not_find_in_iff in Hc; apply Hc. move/mapP in Hm; destruct Hm as [xe Hxe Hm]. rewrite F.elements_in_iff; exists xe.2. rewrite -in_InA_eq_key_elt_iff /m' Hm /= /multinom_of_seqmultinom_val. rewrite /multinom_of_seqmultinom /seqmultinom_of_multinom. case (sumb _) => [prf|] /=. rewrite -map_comp (eq_map spec_NK) map_id -surjective_pairing //. rewrite size_map (@eq_sz xe.1); [by []|exists xe.2]. by apply /M.elements_2 /in_InA_eq_key_elt_iff; rewrite -surjective_pairing. 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)