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