proposition: Lemma Zlcm_den_poly_nz : forall P, Zlcm_den_poly P [#] [0].
proof: Proof. intro P; apply Zlcm_gen_nz. intro a; pattern P; apply Ccpoly_induc; clear P. simpl; intro H; destruct H; [|contradiction]. rewrite <- H; discriminate. intros P c. rewrite den_list_linear. rewrite Q_can_den_pos_val_spec. induction (den_list P). simpl; intros. destruct H0; [rewrite <- H0; discriminate|contradiction]. simpl; intros. destruct H0; [rewrite <- H0; discriminate|]. apply H; assumption. Qed.
imports: CPoly_Degree CoRN.model.rings.Qring Zring Qordfield CRing_Homomorphisms RingClass CRingClass Zlcm Q_can RX_deg