proposition: Lemma cpoly_inv_lin : forall p c, cpoly_inv_cs (cpoly_linear_cs c p) = cpoly_linear_cs [--]c (cpoly_inv_cs p).
proof: Proof. simple induction p; auto. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational