proposition: Lemma _cpoly_lin_eq_zero : forall p c, c [=] [0] /\ p [=] cpoly_zero_cs -> cpoly_linear_cs c p [=] cpoly_zero_cs.
proof: Proof. unfold cpoly_linear_cs in |- *. unfold cpoly_zero_cs in |- *. simpl in |- *. intros p c H. elim H; intros. split; auto. rewrite <- cpoly_eq_p_zero. assumption. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational