proposition: Lemma nth_coeff_Q_can_num_poly_spec : forall P n, nth_coeff n (Q_can_num_poly P) = Q_can_num (nth_coeff n P).
proof: Proof. intro P; pattern P; apply Ccpoly_induc; clear P. simpl; unfold Q_can_num. rewrite Zdiv_0_l; reflexivity. destruct n. reflexivity. rewrite Q_can_num_poly_linear. rewrite -> coeff_Sm_lin. rewrite H. apply Q_can_num_spec. symmetry; apply coeff_Sm_lin. Qed.
imports: CPoly_Degree CoRN.model.rings.Qring Zring Qordfield CRing_Homomorphisms RingClass CRingClass Zlcm Q_can RX_deg