proposition: Lemma degree_le_wd : forall (p p' : RX) n, p [=] p' -> degree_le n p -> degree_le n p'.
proof: Proof. unfold degree_le in |- *. intros. Step_final (nth_coeff m p). Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia