proposition: Lemma RX_deg_wd : forall P Q, P [=] Q -> RX_deg P = RX_deg Q.
proof: Proof. intros P Q; pattern P, Q; apply Ccpoly_double_sym_ind; clear P Q. intros P Q Hsym Heq. symmetry; apply Hsym; symmetry; assumption. intro p; pattern p; apply Ccpoly_induc; clear p. reflexivity. intros. rewrite RX_deg_linear. case (RX_dec p [0]). reflexivity. intro Hap; destruct (ap_imp_neq _ _ _ Hap). apply (linear_eq_zero_ _ _ _ H0). intros P Q c d Hrec Heq. destruct (linear_eq_linear_ _ _ _ _ _ Heq). rewrite RX_deg_linear. rewrite RX_deg_linear. case (RX_dec P [0]). case (RX_dec Q [0]). reflexivity. intros H1 H2; destruct (ap_imp_neq _ _ _ H1). rewrite <- H0; assumption. case (RX_dec Q [0]). intros H1 H2; destruct (ap_imp_neq _ _ _ H2). rewrite -> H0; assumption. intros HQ HP. f_equal; apply Hrec; assumption. Qed.
imports: CPoly_Degree RingClass CRingClass