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