proposition: Lemma nth_coeff_nexp_eq : forall i, nth_coeff i (_X_[^]i) [=] ([1]:R).
proof: Proof. intros. induction i as [| i Hreci]; intros. simpl in |- *. algebra. change (nth_coeff (S i) (_X_[^]i[*]_X_) [=] ([1]:R)) in |- *. Step_final (nth_coeff i (_X_[^]i):R). Qed.
imports: CoRN.algebra.CPolynomials Coq.Classes.Morphisms CoRN.algebra.CRings