proposition: Lemma RX_deg_sum : forall p q, RX_deg p <> RX_deg q -> RX_deg (p[+]q)=Nat.max (RX_deg p) (RX_deg q).
proof: Proof. intros p q Hneq. case (RX_dec p [0]). intro H; rewrite (RX_deg_wd _ _ H). transitivity (RX_deg q); [apply RX_deg_wd; rewrite -> H; unfold RX; ring|]. rewrite RX_deg_zero; reflexivity. case (RX_dec q [0]). intro H; rewrite (RX_deg_wd _ _ H). transitivity (RX_deg p); [apply RX_deg_wd; rewrite -> H; unfold RX; ring|]. rewrite RX_deg_zero; rewrite Nat.max_comm; reflexivity. intros Hq Hp. set (RX_deg_spec _ Hp). set (RX_deg_spec _ Hq). case (le_lt_dec (RX_deg p) (RX_deg q)); intro. rewrite Nat.max_r; [|assumption]. inversion l. destruct (Hneq H0). apply (degree_inj (p[+]q)). apply RX_deg_spec. case (RX_dec (p[+]q) [0]); [|tauto]. intro; destruct Hneq. rewrite (RX_deg_wd p ([--]q)). symmetry; apply RX_deg_inv. apply cg_inv_unique'; assumption. apply (degree_plus_rht _ _ _ m); [| |apply le_n]. apply (degree_le_mon _ _ (RX_deg p)); [assumption|apply d]. rewrite H; apply RX_deg_spec; assumption. rewrite Nat.max_l; [|apply Nat.lt_le_incl; assumption]. apply (degree_inj (p[+]q)). apply RX_deg_spec. case (RX_dec (p[+]q) [0]); [|tauto]. intro; destruct Hneq. rewrite (RX_deg_wd p ([--]q)). symmetry; apply RX_deg_inv. apply cg_inv_unique'; assumption. apply (degree_wd _ _ _ _ (cag_commutes _ _ _)). apply (degree_plus_rht _ _ _ (RX_deg q)); [| |assumption]. apply degree_imp_degree_le. apply RX_deg_spec; assumption. apply RX_deg_spec; assumption. Qed.
imports: CPoly_Degree RingClass CRingClass