proposition: Lemma cpoly_mult_zero : forall p, cpoly_mult_cs p cpoly_zero_cs [=] cpoly_zero_cs.
proof: Proof. intros. pattern p in |- *; apply cpoly_ind_cs. algebra. intros. rewrite cpoly_lin_mult. rewrite cpoly_zero_mult_cr. rewrite cpoly_zero_plus. apply _cpoly_lin_eq_zero. split;algebra. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational