proposition: Lemma cpoly_plus_q_ap_q : forall p q, cpoly_plus_cs p q [#] q -> p [#] cpoly_zero_cs.
proof: Proof. intro p; pattern p in |- *; apply Ccpoly_ind_cs. intro. rewrite cpoly_zero_plus. intro H. exfalso. apply (ap_irreflexive _ _ H). do 4 intro. pattern q in |- *; apply Ccpoly_ind_cs. rewrite cpoly_plus_zero. auto. do 3 intro. rewrite cpoly_lin_plus_lin. intros. cut (c[+]c0 [#] c0 or cpoly_plus_cs p0 p1 [#] p1). intros. 2: apply cpoly_lin_ap_lin_. 2: assumption. cut (c [#] [0] or p0 [#] cpoly_zero_cs). intro. apply _cpoly_lin_ap_zero. assumption. elim X1; intro. left. apply cg_ap_cancel_rht with c0. astepr c0. auto. right. generalize (X _ b); intro. assumption. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational