proposition: Lemma poly_degree_lth : forall p : RX, degree_le (lth_of_poly p) p.
proof: Proof. unfold degree_le in |- *. intros. apply not_ap_imp_eq. intro. elim (proj1 (Nat.lt_nge _ _) H). apply Nat.lt_le_incl. apply lt_i_lth_of_poly. auto. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia