proposition: Lemma Zlcm_den_poly_spec0 : forall P n, nth_coeff n (_C_ (Zlcm_den_poly P:Q_as_CRing) [*] P) [=] Qmake (Zlcm_den_poly P * Qnum (nth_coeff n P)) (Qden (nth_coeff n P)).
proof: Proof. intros P n. rewrite -> nth_coeff_c_mult_p. simpl. generalize (Zlcm_den_poly P), (nth_coeff n P); clear; intros z q. destruct q as [qn qd]; simpl. unfold Qmult; simpl. reflexivity. Qed.
imports: CPoly_Degree CoRN.model.rings.Qring Zring Qordfield CRing_Homomorphisms RingClass CRingClass Zlcm Q_can RX_deg