proposition: Lemma den_div_Pn0 : forall (Q : ZX) (n : nat) (p q : Z_as_CRing), Sum 0 n (fun i : nat => nth_coeff i Q[*]p[^]i[*]q[^](n - i))[=][0] -> Zdivides q (nth_coeff n Q[*]p[^]n).
proof: Proof. clear QX QX_dec QX_deg. intros P n p q. destruct n. rewrite -> Sum_one. simpl. rewrite Zmult_1_r; intro H; rewrite H. apply Zdivides_zero_rht. rewrite -> Sum_last. rewrite Nat.sub_diag. simpl (q[^]0). rewrite -> mult_one. generalize (nth_coeff (S n) P[*]p[^]S n); intro r. exists ([--](Sum 0 n (fun i : nat => nth_coeff i P[*]p[^]i[*]q[^](n - i)))). rewrite Zopp_mult_distr_l_reverse. symmetry; apply (cg_inv_unique Z_as_CRing). rewrite <- H. apply cs_bin_op_wd; [|reflexivity]. rewrite <- (mult_distr_sum_rht Z_as_CRing). apply Sum_wd'. apply Nat.le_0_l. intros i H0 Hn. rewrite <- CRings.mult_assoc. apply mult_wd. reflexivity. rewrite Nat.sub_succ_l; [|assumption]. reflexivity. Qed.
imports: CPoly_Degree CRing_Homomorphisms Qring Zring Qordfield RingClass CRingClass Zlcm Q_can nat_Q_lists RX_deg QX_ZX