proposition: Lemma degree_inv : forall (p : RX) (n : nat), degree n p -> degree n [--]p.
proof: Proof. unfold degree in |- *. intros p n H. elim H. clear H. intros. split. astepl ( [--] (nth_coeff n p)). algebra. apply degree_le_inv; auto. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia