proposition: Lemma Q_can_num_poly_spec : forall P Q, P [=] Q -> Q_can_num_poly P [=] Q_can_num_poly Q.
proof: Proof. intros P Q; pattern P, Q; apply Ccpoly_double_sym_ind; clear P Q. intros P Q Hsym Heq. symmetry; apply Hsym; symmetry; assumption. intro P. pattern P; apply Ccpoly_induc; clear P. reflexivity. intros P c Hrec Heq. destruct (zero_eq_linear_ _ _ _ Heq). split. rewrite (Q_can_num_spec _ [0]). reflexivity. assumption. change ([0] [=] Q_can_num_poly P). symmetry; apply Hrec; symmetry; assumption. intros P Q c d Hrec Heq. destruct (linear_eq_linear_ _ _ _ _ _ Heq). rewrite Q_can_num_poly_linear, Q_can_num_poly_linear. apply _linear_eq_linear. split. apply Q_can_num_spec; assumption. apply Hrec; assumption. Qed.
imports: CPoly_Degree CoRN.model.rings.Qring Zring Qordfield CRing_Homomorphisms RingClass CRingClass Zlcm Q_can RX_deg