proposition: Lemma qx2zx_deg : forall P, QX_deg P = ZX_deg (qx2zx P).
proof: Proof. intro P; unfold qx2zx. rewrite <- Q_can_num_poly_deg_eq. symmetry; apply RX_deg_cmult_p. intro; apply (Zlcm_den_poly_nz P). rewrite (injZ_spec2 (Zlcm_den_poly P)). revert H; generalize (inject_Z (Zlcm_den_poly P)); clear. intro q; destruct q as [qn qd]. unfold Qeq, Q_can_num; simpl. rewrite Zmult_1_r; intro H; rewrite H. compute; reflexivity. Qed.
imports: CPoly_Degree CRing_Homomorphisms Qring Zring Qordfield RingClass CRingClass Zlcm Q_can nat_Q_lists RX_deg QX_ZX