proposition: Lemma Q_can_num_poly_linear : forall c P, Q_can_num_poly (c[+X*]P) = Q_can_num c[+X*]Q_can_num_poly P.
proof: Proof. reflexivity. Qed.
imports: CPoly_Degree CoRN.model.rings.Qring Zring Qordfield CRing_Homomorphisms RingClass CRingClass Zlcm Q_can RX_deg