proposition: Lemma monic_apzero : forall (p : RX) n, monic n p -> p [#] [0].
proof: Proof. unfold monic in |- *. intros. elim H. clear H. intros. apply nth_coeff_ap_zero_imp with n. astepl ([1]:R). apply one_ap_zero. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia