proposition: Lemma QX_div_deg0 : forall (p : QX) (a : Q_as_CRing), QX_deg p <> 0 -> RX_div _ p a [#] [0].
proof: Proof. intros p a Hdeg. case (QX_dec (RX_div _ p a) [0]); [|tauto]. intro Heq; destruct Hdeg; revert Heq. unfold RX_div. destruct (cpoly_div p (_X_monic _ a)) as [[q r] _ [s [d s0]]]. unfold fst, snd in *. intro Hq. rewrite -> Hq in s. assert (H : p [=] r); [rewrite -> s; unfold cg_minus; unfold QX; ring|]. unfold QX_deg; rewrite (RX_deg_wd _ Q_dec _ _ H); fold QX_deg. destruct (_X_monic _ a). destruct (degree_le_zero _ _ (d _ H1)). unfold QX_deg; rewrite (RX_deg_wd _ Q_dec _ _ s1). rewrite RX_deg_c_; reflexivity. 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