proposition: Lemma den_list_spec : forall P n, n <= QX_deg P -> In (Q_can_den (nth_coeff n P)) (den_list P).
proof: Proof. intro P; pattern P; apply Ccpoly_induc; clear P. simpl; left. rewrite Q_can_den_pos_val_spec. unfold Q_can_den_pos_val; reflexivity. intros P c Hrec n. unfold QX_deg; rewrite RX_deg_linear; fold QX_deg; fold QX_dec. case (QX_dec P [0]). simpl. case n. left; reflexivity. intros A B C; inversion C. intros Hap Hle. simpl. destruct n. left; reflexivity. right; apply Hrec. apply le_S_n; assumption. Qed.
imports: CPoly_Degree CoRN.model.rings.Qring Zring Qordfield CRing_Homomorphisms RingClass CRingClass Zlcm Q_can RX_deg