proposition: Lemma cpoly_mult_fast_ap_equiv : forall p1 p2 q1 q2, (cpoly_mult_fast_cs p1 q1)[#](cpoly_mult_cs p2 q2) -> p1[#]p2 or q1[#]q2.
proof: Proof. destruct q1 as [|c q1]; destruct q2 as [|c0 q2]; intros X; simpl in X. Proof. rewrite cpoly_ap_p_zero in X. elim (ap_irreflexive cpoly_csetoid cpoly_zero). stepl (cpoly_mult_cs p2 cpoly_zero). assumption. apply cpoly_mult_zero. rewrite cpoly_ap_p_zero in X. right. apply ap_symmetric. eapply cring_mult_ap_zero_op with (R:=cpoly_cring_old). apply X. right. eapply cring_mult_ap_zero_op with (R:=cpoly_cring_old). change (cpoly_mult p1 (cpoly_linear c q1)) with (cpoly_mult_cs p1 (cpoly_linear c q1)) in X. stepr (cpoly_mult_cs p2 cpoly_zero). apply X. apply cpoly_mult_zero. apply cpoly_mult_op_strext. apply X. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational