proposition: Lemma monic_cpoly_linear : forall (p : cpoly R) c n, monic (S n) (c[+X*]p) -> monic n p.
proof: Proof. unfold monic in |- *. intros. elim H. clear H. intros. split. auto. apply degree_le_cpoly_linear with c. auto. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia