proposition: Lemma degree_nexp : forall (p : FX) m n, degree m p -> degree (m * n) (p[^]n).
proof: Proof. intros. induction n as [| n Hrecn]; intros. replace (m * 0) with 0. apply degree_wd with (_C_ ([1]:F)). algebra. apply degree_c_. algebra. auto. replace (m * S n) with (m * n + m). apply degree_wd with (p[^]n[*]p). algebra. apply degree_mult; auto. auto. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia