proposition: Lemma nth_coeff_nexp_neq : forall i j, i <> j -> nth_coeff i (_X_[^]j) [=] ([0]:R).
proof: Proof. intro; induction i as [| i Hreci]; intros; [ induction j as [| j Hrecj] | induction j as [| j Hrecj] ]; intros. elim (H (refl_equal _)). Step_final (nth_coeff 0 (_X_[*]_X_[^]j):R). simpl in |- *. algebra. change (nth_coeff (S i) (_X_[^]j[*]_X_) [=] ([0]:R)) in |- *. astepl (nth_coeff i (_X_[^]j):R). apply Hreci. auto. Qed.
imports: CoRN.algebra.CPolynomials Coq.Classes.Morphisms CoRN.algebra.CRings