proposition: Lemma monom_coeff : forall (c : R) n, nth_coeff n (monom c n) [=] c.
proof: Proof. intros. induction n as [| n Hrecn]; intros. simpl in |- *. algebra. simpl in |- *. algebra. Qed.
imports: CoRN.algebra.CPoly_Degree Coq(Lia)