proposition: Lemma cpoly_ap_zero_plus : forall p q, cpoly_plus_cs p q [#] cpoly_zero_cs -> p [#] cpoly_zero_cs or q [#] cpoly_zero_cs.
proof: Proof. intros p q; pattern p, q in |- *; apply Ccpoly_double_sym_ind0_cs. unfold Csymmetric in |- *. intros x y H H0. elim H. auto. auto. astepl (cpoly_plus_cs y x). auto. apply cpoly_plus_commutative. intros p0 H. left. rewrite cpoly_plus_zero in H. assumption. intros p0 q0 c d. rewrite cpoly_lin_plus_lin. intros. cut (c[+]d [#] [0] or cpoly_plus_cs p0 q0 [#] cpoly_zero_cs). 2: apply cpoly_lin_ap_zero_. 2: assumption. clear X0. intros H0. elim H0; intro H1. cut (c[+]d [#] [0][+][0]). intro H2. elim (cs_bin_op_strext _ _ _ _ _ _ H2); intro H3. left. simpl in |- *. left. assumption. right. cut (d [#] [0] or q0 [#] cpoly_zero_cs). intro H4. apply _cpoly_lin_ap_zero. auto. left. assumption. astepr ([0]:CR). auto. elim (X H1); intro. left. cut (c [#] [0] or p0 [#] cpoly_zero_cs). intro; apply _cpoly_lin_ap_zero. auto. right. assumption. right. cut (d [#] [0] or q0 [#] cpoly_zero_cs). intro. apply _cpoly_lin_ap_zero. auto. right. assumption. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational