proposition: Lemma RX_deg_x_ : RX_deg _X_ = 1.
proof: Proof. simpl. case (RX_dec (cpoly_one R) (cpoly_zero R)). intro H; destruct (eq_imp_not_ap _ _ _ H (ring_non_triv _)). intro; case (RX_dec (cpoly_zero R) (cpoly_zero R)); [reflexivity|]. intro H; destruct (ap_irreflexive _ _ H). Qed.
imports: CPoly_Degree RingClass CRingClass