proposition: Lemma QX_normalize_spec : forall p : QX, p [#] [0] -> monic (QX_deg p) ((_C_ (QX_normalize p)) [*] p).
proof: Proof. intros p H. destruct (RX_deg_spec _ Q_dec _ H) as [Hcoeff Hdeg]. split. rewrite -> nth_coeff_c_mult_p. unfold QX_normalize. case (Qeq_dec (nth_coeff (QX_deg p) p) [0]). intro; destruct Hcoeff; assumption. intro Hap. apply (div_1 Q_as_CField). intros m Hlt; rewrite -> nth_coeff_c_mult_p. rewrite -> (Hdeg m Hlt). ring. Qed.
imports: CPoly_Degree CoRN.model.rings.Qring Zring Qordfield CRing_Homomorphisms RingClass CRingClass Zlcm Q_can RX_deg