proposition: Lemma den_div_Pn : forall (P : QX) (a : Q_as_CRing), P ! a [=] [0] -> Zdivides (Q_can_den a) (Pn P).
proof: Proof. intros P a Hval. rewrite Q_can_den_pos_val_spec. apply (Zrelprime_div_mult_intro _ ((Q_can_num a:Z_as_CRing)[^]QX_deg P)). apply Zrelprime_nexp. apply Zrelprime_symm. apply (Q_can_spec2 a). rewrite Zmult_comm. apply (den_div_Pn1 _ (Q_can a)). rewrite <- Hval. apply cpoly_apply_wd; [reflexivity|]. symmetry; apply Q_can_spec. Qed.
imports: CPoly_Degree CRing_Homomorphisms Qring Zring Qordfield RingClass CRingClass Zlcm Q_can nat_Q_lists RX_deg QX_ZX