proposition: Lemma Zlcm_den_poly_spec : forall P, in_ZX (_C_ (Zlcm_den_poly P:Q_as_CRing) [*] P).
proof: Proof. intros P n. unfold in_Z. case (le_lt_dec n (QX_deg P)). transitivity (Q_can_den ((Qmake (Zlcm_den_poly P) xH) [*] nth_coeff n P)). apply Q_can_den_spec. apply nth_coeff_c_mult_p. simpl; unfold Qmult; simpl. rewrite -> den_1_div_iff. unfold Qmult; simpl. unfold Zlcm_den_poly. rewrite (Zgcd_div_mult_rht (Qnum (nth_coeff n P)) (Qden (nth_coeff n P))); try (intro H0; destruct (Zgcd_zero _ _ H0); discriminate). fold (Q_can_den (nth_coeff n P)). apply Zdivides_mult_elim; try apply Zgcd_is_divisor_lft. apply Zlcm_gen_spec. apply den_list_spec; assumption. intros Hgt. cut (nth_coeff n (_C_ (Zlcm_den_poly P:Q_as_CRing)[*]P) [=] [0]). intro Heq. transitivity (Q_can_den [0]). apply Q_can_den_spec; assumption. rewrite Q_can_den_pos_val_spec; reflexivity. case (RX_dec _ Q_dec P [0]). intro H. transitivity (nth_coeff n ([0]:QX)). apply nth_coeff_wd. rewrite -> H at 2. apply I. reflexivity. intro Hap. rewrite -> nth_coeff_c_mult_p. cut (nth_coeff n P [=] [0]). intro H; rewrite -> H; ring. cut (degree_le (QX_deg P) P). intro H; apply H; assumption. destruct (RX_deg_spec _ Q_dec P); assumption. Qed.
imports: CPoly_Degree CoRN.model.rings.Qring Zring Qordfield CRing_Homomorphisms RingClass CRingClass Zlcm Q_can RX_deg