proposition: Lemma RX_deg_spec : forall p : RX, p [#] [0] -> degree (RX_deg p) p.
proof: Proof. intro p; pattern p; apply Ccpoly_induc; clear p. intro H; destruct (ap_irreflexive _ _ H). unfold RX; intros p c Hrec. rewrite linear_ap_zero; intro H. rewrite RX_deg_linear. case (RX_dec p [0]). case H. split. assumption. intro m; case m. intro H1; inversion H1. intros; rewrite -> coeff_Sm_lin. rewrite <- (nth_coeff_zero _ n). apply nth_coeff_wd; assumption. intros Hap Heq; destruct (eq_imp_not_ap _ _ _ Heq Hap). intro H0; destruct (Hrec H0) as [Hcoeff Hdeg]. split. case (R_dec (nth_coeff (S (RX_deg p)) (c[+X*]p)) [0]). intro H1; destruct (ap_imp_neq _ _ _ Hcoeff). rewrite -> coeff_Sm_lin in H1; assumption. tauto. intro m; case m. intro H1; inversion H1. clear m; intros m Hlt; rewrite -> coeff_Sm_lin. apply Hdeg; apply le_S_n; assumption. Qed.
imports: CPoly_Degree RingClass CRingClass