proposition: Lemma Q_can_num_poly_deg_eq : forall P, QX_deg P = ZX_deg (Q_can_num_poly P).
proof: Proof. intro P. pattern P; apply Ccpoly_induc; clear P. reflexivity. intros P c Heq. rewrite Q_can_num_poly_linear. unfold QX_deg, ZX_deg. rewrite RX_deg_linear; fold QX_dec. rewrite RX_deg_linear; fold ZX_dec. fold QX_deg; fold ZX_deg. rewrite <- Heq. case (QX_dec P [0]). case (ZX_dec (Q_can_num_poly P) [0]). reflexivity. intros Hap Heq2; destruct (ap_imp_neq _ _ _ Hap); revert Heq2; clear. pattern P; apply Ccpoly_induc; clear P. reflexivity. intros P c Hrec Heq; destruct (linear_eq_zero_ _ _ _ Heq). rewrite Q_can_num_poly_linear. apply _linear_eq_zero; split. rewrite (Q_can_num_spec _ _ H); reflexivity. apply Hrec; assumption. intro Hap; case (ZX_dec (Q_can_num_poly P) [0]). intro Heq2; destruct (ap_imp_neq _ _ _ Hap); revert Heq2; clear. pattern P; apply Ccpoly_induc; clear P. reflexivity. intros P c Hrec Heq. rewrite Q_can_num_poly_linear in Heq. destruct (linear_eq_zero_ _ _ _ Heq). apply _linear_eq_zero; split; [|apply Hrec; assumption]. revert H; clear; destruct c as [qn qd]. unfold Q_can_num; simpl; unfold Qeq; simpl. rewrite Zmult_1_r. intro H; rewrite (Zgcd_div_mult_lft qn qd). rewrite H. apply Zmult_0_l. intro H0; destruct (Zgcd_zero _ _ H0); discriminate. reflexivity. Qed.
imports: CPoly_Degree CoRN.model.rings.Qring Zring Qordfield CRing_Homomorphisms RingClass CRingClass Zlcm Q_can RX_deg