proposition: Lemma symmetric_cpoly_ap : Csymmetric cpoly_ap.
proof: Proof. red in |- *. intros x y. pattern x, y in |- *. apply Ccpoly_double_ind0'. simpl in |- *; simple induction p; auto. simpl in |- *; auto. simpl in |- *. intros p q c d H H0. elim H0; intro H1. left. apply ap_symmetric_unfolded. assumption. auto. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational