proposition: Lemma refine_find_mpoly (n : nat) T (p : mpoly n T) (p' : effmpoly T) : refines Reffmpoly p p' -> forall m m', refines Rseqmultinom m m' -> p@_m = odflt 0 (M.find m' p').
proof: Proof. rewrite !refinesE /Reffmpoly /mpoly_of_effmpoly /ofun_hrel. set t := P.for_all _ _; case_eq t => //. rewrite /t (P.for_all_iff _); [|by move=> m _ /mnmc_eq_seqP /eqP <-]. move=> H_sz H; injection H; move=> {}H m m' Hm'. rewrite -H 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 /(H_sz _ xe.2) /M.elements_2. by apply in_InA_eq_key_elt_iff; rewrite -surjective_pairing. } move: Hy; move/mapP => [ye Hye ->]. apply/eqP /(H_sz _ ye.2) /M.elements_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. move: Hm'; rewrite /Rseqmultinom /ofun_hrel /multinom_of_seqmultinom_val. by case (multinom_of_seqmultinom n m') => // m'' Hm''; injection Hm''. } 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. suff: m' = xe.1; [by move=> ->; rewrite -surjective_pairing|]. move: Hm' Hm; rewrite /Rseqmultinom /ofun_hrel /multinom_of_seqmultinom_val /=. rewrite /multinom_of_seqmultinom /seqmultinom_of_multinom. case (sumb _) => [prf|] //= Hm; injection Hm; move=> <- {Hm}. case (sumb _) => [prf'|] //=. by move=> H'; inversion H'; apply: map_spec_N_inj. rewrite size_map => Hf _. rewrite size_map in prf. rewrite (H_sz xe.1 xe.2) in Hf => //; apply M.elements_2. by rewrite -in_InA_eq_key_elt_iff -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)