proposition: Lemma QX_integral : forall p q : QX, p [#] [0] -> q [#] [0] -> p[*]q [#] [0].
proof: Proof. intros p q Hp Hq. apply (nth_coeff_strext _ (QX_deg p + QX_deg q)). simpl (nth_coeff (QX_deg p + QX_deg q) ([0]:QX)). cut (degree (QX_deg p + QX_deg q) (p[*]q)). intro H; apply H. apply (degree_mult Q_as_CField). apply RX_deg_spec; assumption. apply RX_deg_spec; assumption. Qed.
imports: CPoly_Degree CRing_Homomorphisms CoRN.model.ordfields.Qordfield CauchySeq Q_in_CReals CPoly_Euclid RingClass CRingClass Q_can nat_Q_lists RX_deg RX_div QX_root_loc