proposition: Lemma degree_le_nexp : forall (p : RX) m n, degree_le m p -> degree_le (m * n) (p[^]n).
proof: Proof. intros. induction n as [| n Hrecn]; intros. replace (m * 0) with 0. apply degree_le_wd with (_C_ ([1]:R)). algebra. apply degree_le_c_. auto. replace (m * S n) with (m * n + m). apply degree_le_wd with (p[^]n[*]p). algebra. apply degree_le_mult; auto. auto. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia