proposition: Lemma cpoly_one_mult : forall p, cpoly_mult_cs cpoly_one p [=] p.
proof: Proof. intro. unfold cpoly_one in |- *. unfold cpoly_constant in |- *. replace (cpoly_linear [1] cpoly_zero) with (cpoly_linear_cs [1] cpoly_zero). 2: reflexivity. rewrite cpoly_lin_mult. rewrite cpoly_zero_mult. apply eq_transitive_unfolded with (cpoly_plus_cs p cpoly_zero_cs). apply cpoly_plus_op_wd. apply cpoly_mult_cr_one. apply _cpoly_lin_eq_zero; algebra. rewrite cpoly_plus_zero; algebra. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational