proposition: Lemma RX_deg_c_ : forall a : R, RX_deg (_C_ a) = 0.
proof: Proof. simpl; case (RX_dec (cpoly_zero R) (cpoly_zero R)); [reflexivity|]. intro H; destruct (ap_irreflexive _ _ H). Qed.
imports: CPoly_Degree RingClass CRingClass