proposition: Lemma QX_deg_mult : forall p q, p [#] [0] -> q [#] [0] -> QX_deg (p[*]q) = QX_deg p + QX_deg q.
proof: Proof. intros p q Hp Hq. set (RX_deg_spec _ Q_dec _ Hp). set (RX_deg_spec _ Q_dec _ Hq). set (degree_mult Q_as_CField _ _ _ _ d d0). fold QX_deg in d1. apply (degree_inj _ (p[*]q)); [|assumption]. apply RX_deg_spec. apply QX_integral; 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