proposition: Lemma QX_div_deg : forall (p : QX) (a : Q_as_CRing), QX_deg p <> 0 -> QX_deg p = S (QX_deg (RX_div _ p a)).
proof: Proof. intros p a Hdeg. case_eq (QX_deg p). intro; destruct Hdeg; assumption. intros n Heq. f_equal. revert Heq. unfold QX_deg; rewrite (RX_deg_wd _ Q_dec _ _ (RX_div_spec _ p a)). rewrite RX_deg_sum. rewrite Nat.max_comm. rewrite -> QX_deg_mult. unfold QX_deg; rewrite RX_deg_minus. rewrite RX_deg_c_, RX_deg_x_, RX_deg_c_; fold QX_deg. simpl; rewrite Nat.add_comm; simpl. intro H; injection H; symmetry; assumption. rewrite RX_deg_x_, RX_deg_c_; discriminate. apply QX_div_deg0; assumption. right; left; discriminate. rewrite RX_deg_c_. rewrite -> QX_deg_mult. unfold QX_deg; rewrite RX_deg_minus. rewrite RX_deg_x_, RX_deg_c_. rewrite Nat.add_comm; discriminate. rewrite RX_deg_x_, RX_deg_c_; discriminate. apply QX_div_deg0; assumption. right; left; discriminate. 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