proposition: Lemma RX_deg_minus : forall p q, RX_deg p <> RX_deg q -> RX_deg (p[-]q)=Nat.max (RX_deg p) (RX_deg q).
proof: Proof. unfold cg_minus; intros p q Hneq. rewrite (RX_deg_inv q) in Hneq. rewrite (RX_deg_sum _ _ Hneq). f_equal. symmetry; apply RX_deg_inv. Qed.
imports: CPoly_Degree RingClass CRingClass