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