proposition: Lemma nth_coeff_inv' : forall (p : RX) i, nth_coeff i (cpoly_inv _ p) [=] [--] (nth_coeff i p).
proof: Proof. intros. change (nth_coeff i [--] (p:RX) [=] [--] (nth_coeff i p)) in |- *. algebra. Qed.
imports: CoRN.algebra.CPolynomials Coq.Classes.Morphisms CoRN.algebra.CRings