proposition: Lemma cpoly_mult_cr_one : forall p, cpoly_mult_cr_cs p [1] [=] p.
proof: Proof. intro. pattern p in |- *; apply cpoly_ind_cs. algebra. intros. rewrite cpoly_lin_mult_cr. apply _cpoly_lin_eq_lin. algebra. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational