proposition: Lemma degree_inj : forall (P : RX) m n, degree m P -> degree n P -> m = n.
proof: Proof. intros P m n Hm Hn. destruct Hm as [Hm1 Hm2]. destruct Hn as [Hn1 Hn2]. case (lt_eq_lt_dec m n). intro H; destruct H. destruct (ap_imp_neq _ _ _ Hn1). apply Hm2; assumption. assumption. intro Hlt; destruct (ap_imp_neq _ _ _ Hm1). apply Hn2; assumption. Qed.
imports: CPoly_Degree RingClass CRingClass