proposition: Lemma Q_Z_poly_apply : forall (P : ZX) (p : Z_as_CRing) (q : positive), let n := ZX_deg P in (q:Q_as_CRing)[^]n [*] (zx2qx P) ! (p # q)%Q [=] Sum 0 n (fun i => (nth_coeff i P) [*] p [^] i [*] (q : Z_as_CRing)[^](n - i)).
proof: Proof. intros P p q n. assert (degree_le n (zx2qx P)). case (ZX_dec P [0]). intro H; apply (degree_le_wd _ (_C_ [0])). rewrite -> H; split; [reflexivity|apply I]. apply (degree_le_mon _ _ 0). apply Nat.le_0_l. apply degree_le_c_. intro Hap. destruct (RX_deg_spec _ Z_dec _ Hap). clear c; fold (ZX_deg P) in d; fold n in d. intros m Hlt. rewrite -> nth_coeff_zx2qx. rewrite d; [reflexivity|assumption]. rewrite -> (poly_as_sum _ _ _ H). rewrite <- mult_distr_sum_lft. rewrite -> (Sum_ring_hom _ _ injZ_rh). apply Sum_wd'. apply Nat.le_0_l. intros i H0 Hn. rewrite -> nth_coeff_zx2qx. rewrite -> rh_pres_mult. rewrite -> rh_pres_mult. rewrite -> mult_commutes. rewrite -> nexp_ring_hom, nexp_ring_hom. rewrite <- CRings.mult_assoc, <- CRings.mult_assoc. apply mult_wdr. rewrite <- (Nat.sub_add _ _ Hn) at 1. rewrite Nat.add_comm. clear H0 Hn. rewrite <- nexp_plus. rewrite -> CRings.mult_assoc. apply mult_wdl. simpl (injZ_rh p). rewrite -> (Q_Z_nexp p q i). apply (nexp_ring_hom _ _ injZ_rh). Qed.
imports: CPoly_Degree CRing_Homomorphisms Qring Zring Qordfield RingClass CRingClass Zlcm Q_can nat_Q_lists RX_deg QX_ZX