proposition: Lemma monic_minus : forall (p q : RX) m n, degree_le m p -> monic n q -> m < n -> monic n (q[-]p).
proof: Proof. intros. apply monic_wd with ( [--]p[+]q). Step_final (q[+][--]p). apply monic_plus with m. apply degree_le_inv. auto. auto. auto. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia