proposition: Lemma monom_coeff' : forall (c : R) m n, m <> n -> nth_coeff n (monom c m) [=] [0].
proof: Proof. intros c m. induction m as [| m Hrecm]; intros. elim (O_or_S n); intro y. elim y. clear y. intros x y. rewrite <- y. simpl in |- *. algebra. elim (H y). elim (O_or_S n); intro y. elim y. clear y. intros x y. rewrite <- y. simpl in |- *. apply Hrecm. lia. rewrite <- y. simpl in |- *. algebra. Qed.
imports: CoRN.algebra.CPoly_Degree Coq(Lia)