proposition: Lemma RX_dec : forall p q : RX, sum (p [=] q) (p [#] q).
proof: Proof. unfold RX; intros p q; pattern p, q; apply Ccpoly_double_sym_ind; clear p q. intros p q H. case H. left; symmetry; assumption. right; apply ap_symmetric; assumption. intro p; pattern p; apply Ccpoly_induc; clear p. left; reflexivity. intros p c; case (R_dec c [0]). intros H1 H2; destruct H2. left; apply _linear_eq_zero; split; assumption. right; rewrite linear_ap_zero; right; assumption. right; rewrite linear_ap_zero; left; assumption. intros p q c d H; case (R_dec c d). case H. left; apply _linear_eq_linear; split; assumption. right; rewrite linear_ap_linear; right; assumption. right; rewrite linear_ap_linear; left; assumption. Qed.
imports: CPoly_Degree RingClass CRingClass