proposition: Lemma refine_comp_monomial_eff n k : refines (Rseqmultinom ==> eq ==> @seq_Reffmpoly n k ==> Reffmpoly) (fun m c lq => mpolyC c * mmap1 (tnth lq) m) (comp_monomial_eff (n:= n)).
proof: Proof. apply refines_abstr => m m' ref_m. apply refines_abstr => c c' ref_c. rewrite refinesE in ref_c; rewrite -{}ref_c {c'}. apply refines_abstr => lq lq' ref_lq. rewrite mul_mpolyC /comp_monomial_eff; eapply refines_apply. { eapply refines_apply; [apply refine_mpoly_scale_eff|by apply trivial_refines]. } move: ref_lq; rewrite refinesE /seq_Reffmpoly; move => [sz_lq ref_lq]. elim: k m m' ref_m lq lq' sz_lq ref_lq =>[|k IHk] m m' ref_m lq lq' sz_lq ref_lq. { rewrite /mmap1 bigop.big_ord0. move: (size0nil sz_lq) => ->; rewrite /zipwith /=; apply refine_mp1_eff. } move: sz_lq; case_eq lq' => //= q0 lqt' Hlq' sz_lq. move: (@refine_size _ _ _ ref_m); case_eq m' => //= m0 mt' Hm' sz_m'. rewrite /foldr /= -/(foldr _ _) /mmap1 bigop.big_ord_recl. eapply refines_apply; [eapply refines_apply; [by apply refine_mpoly_mul_eff|]|]. { move: (@refine_nth _ _ _ ord0 ref_m); rewrite Hm' /= => <-. refines_apply. replace (tnth _ _) with (lq`_O); [|by case lq, tval]. change q0 with (nth mp0_eff (q0 :: lqt') O); rewrite -Hlq'; apply ref_lq. } injection sz_lq => {}sz_lq; injection sz_m' => {}sz_m'. assert (ref_mt : refines Rseqmultinom (multinom_of_seqmultinom_val k mt') mt'). { by apply /refine_multinom_of_seqmultinom_val /eqP. } have Hlq_lq' : forall i : nat, refines Reffmpoly [tuple of behead lq]`_i (nth mp0_eff lqt' i). { by move=> i; move: (ref_lq i.+1); rewrite Hlq' /=; case tval; elim i. } move: (IHk _ _ ref_mt [tuple of behead lq] _ sz_lq Hlq_lq'). rewrite refinesE /Reffmpoly /ofun_hrel => ->; f_equal. apply bigop.eq_big => // i _; f_equal. { rewrite tnth_behead; f_equal. by apply ord_inj; rewrite inordK //; move: (ltn_ord i). } move /eqP in sz_m'; move: (refine_multinom_of_seqmultinom_val sz_m') => Hmt'. move: (@refine_nth _ _ _ i Hmt') => <-. move: (@refine_nth _ _ _ (inord i.+1) ref_m); rewrite Hm' /=. rewrite inordK /=; [|by rewrite ltnS]; move=> ->; apply f_equal. by apply ord_inj; rewrite inordK //; move: (ltn_ord i). 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)