proposition: Lemma cpoly_mult_fast_equiv : forall p q, (cpoly_mult_fast_cs p q)[=](cpoly_mult_cs p q).
proof: Proof. intros p q. apply not_ap_imp_eq. intro H. assert (p[#]p or q[#]q). apply cpoly_mult_fast_ap_equiv. assumption. destruct X as [X|X]; apply (ap_irreflexive _ _ X). Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational