proposition: Lemma monic_plus : forall (p q : RX) m n, degree_le m p -> monic n q -> m < n -> monic n (p[+]q).
proof: Proof. unfold monic in |- *. unfold degree_le in |- *. intros. elim H0. clear H0. intros. split. astepl (nth_coeff n p[+]nth_coeff n q). astepl ([0][+]nth_coeff n q). Step_final (nth_coeff n q). intros. astepl (nth_coeff m0 p[+]nth_coeff m0 q). cut (m < m0). intro. Step_final ([0][+] ([0]:R)). apply Nat.lt_trans with n; auto. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia