proposition: Lemma RX_deg_cmult_p : forall P a, a [#] [0] -> QX_deg (_C_ a [*] P) = QX_deg P.
proof: Proof. intros P a Hap. case (QX_dec P [0]). intro; apply RX_deg_wd. rewrite -> s; ring. intro HapP. apply (degree_inj _ (_C_ a [*] P)). case (QX_dec (_C_ a[*]P) [0]). intro Heq; destruct (ap_imp_neq _ _ _ HapP); clear HapP. apply all_nth_coeff_eq_imp. intro i; generalize (nth_coeff_wd _ i _ _ Heq). rewrite -> nth_coeff_c_mult_p. fold QX; simpl (nth_coeff i ([0]:QX)). intro Heq2; apply (mult_eq_zero _ a); [apply Hap|assumption]. apply RX_deg_spec. destruct (RX_deg_spec _ Q_dec _ HapP). split. intro. destruct c. rewrite -> nth_coeff_c_mult_p in H. apply (mult_eq_zero _ _ _ Hap H). intros m Hlt. rewrite -> nth_coeff_c_mult_p. rewrite -> (d m Hlt); ring. Qed.
imports: CPoly_Degree CRing_Homomorphisms Qring Zring Qordfield RingClass CRingClass Zlcm Q_can nat_Q_lists RX_deg QX_ZX