proposition: Lemma nth_coeff_inv : forall (p : RX) n, nth_coeff n [--]p [=] [--] (nth_coeff n p).
proof: Proof. intro. pattern p in |- *. apply cpoly_induc. intros. simpl in |- *. algebra. intros. elim n. simpl in |- *. algebra. intros. simpl in |- *. apply H. Qed.
imports: CoRN.algebra.CPolynomials Coq.Classes.Morphisms CoRN.algebra.CRings