proposition: Lemma monic_one : forall (p : cpoly R) c, monic 1 (c[+X*]p) -> forall x, p ! x [=] [1].
proof: Proof. intros. cut (monic 0 p). unfold monic in |- *. intros. elim H0. clear H0. intros H0 H1. elim (degree_le_zero _ H1). intro d. intros. astepl (_C_ d) ! x. astepl d. astepl (nth_coeff 0 (_C_ d)). Step_final (nth_coeff 0 p). apply monic_cpoly_linear with c. auto. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia