proposition: Lemma den_div_P01 : forall (P : QX) (a : Q_as_CRing), P ! a [=] [0] -> Zdivides (Qnum a) (P0 P[*](Qden a:Z_as_CRing)[^]QX_deg P).
proof: Proof. intros P a Hval. set (Q := _C_ (Zlcm_den_poly P:Q_as_CRing)[*]P). assert (H : Q ! a [=] [0]). unfold Q; rewrite -> mult_apply, c_apply, Hval; ring. clear Hval; revert H. rewrite -> (zx2qx_spec Q); [|apply Zlcm_den_poly_spec]. unfold Q; clear Q. destruct a as [p q]; unfold Qnum, Qden. set (Q := qx2zx P). intro Hval. assert ((q:Q_as_CRing)[^](ZX_deg Q) [*] (zx2qx Q) ! (p # q)%Q [=] [0]). unfold Q. rewrite -> Hval; ring. assert (Q_can_num ((q:Q_as_CRing)[^](ZX_deg Q) [*] (zx2qx Q) ! (p # q)%Q) [=] [0]). rewrite (Q_can_num_spec _ _ H). unfold Q_can_num; simpl. rewrite Zgcd_one_rht, Zdiv_0_l; reflexivity. clear Hval H; revert H0. rewrite (Q_can_num_spec _ _ (Q_Z_poly_apply _ _ _)). rewrite <- injZ_spec2. assert (ZX_deg Q = QX_deg P). symmetry; apply qx2zx_deg. assert (nth_coeff 0 (qx2zx P) = nth_coeff 0 Q). reflexivity. unfold Q. unfold P0; rewrite H0. rewrite <- H; clear H H0. apply den_div_P00. Qed.
imports: CPoly_Degree CRing_Homomorphisms Qring Zring Qordfield RingClass CRingClass Zlcm Q_can nat_Q_lists RX_deg QX_ZX