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