proposition: Lemma RX_deg_inv : forall p, RX_deg p = RX_deg ([--]p).
proof: Proof. intro p. case (RX_dec p [0]). intro H; rewrite (RX_deg_wd _ _ H), RX_deg_zero. rewrite <- RX_deg_zero; apply RX_deg_wd; rewrite -> H; unfold RX; ring. intro Hp. apply (degree_inj p). apply RX_deg_spec; assumption. apply (degree_wd _ ([--][--]p)); [apply cg_inv_inv|]. apply degree_inv. apply RX_deg_spec. apply inv_resp_ap_zero; assumption. Qed.
imports: CPoly_Degree RingClass CRingClass