proposition: Lemma cpoly_mult_one : forall p, cpoly_mult_cs p cpoly_one [=] p.
proof: Proof. intro. apply eq_transitive_unfolded with (cpoly_mult_cs cpoly_one p). apply cpoly_mult_commutative. apply cpoly_one_mult. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational