proposition: Lemma Liouville_lemma5 : forall (p : Z_as_CRing) (q : positive), (zx2qx P) ! (p#q)%Q [#] [0] -> [1] [<=] (inj_Q_rh q)[^](ZX_deg P) [*] AbsIR (inj_Q_rh ((zx2qx P) ! (p#q)%Q)).
proof: Proof. intros p q Hap. set (n := ZX_deg P). assert (Zpos q=Z.abs q); [reflexivity|]. rewrite H; clear H. rewrite <- nexp_ring_hom. assert (((Z.abs q):Q_as_CRing)[^]n [=] Z.abs ((q:Z_as_CRing)[^]n)). generalize n; clear; induction n; [reflexivity|]. rewrite <- nexp_Sn. rewrite <- nexp_Sn. rewrite Zabs_Zmult. rewrite -> IHn. reflexivity. rewrite -> H; clear H. rewrite <- (AbsIR_Qabs ((q:Z_as_CRing)[^]n)). rewrite <- AbsIR_resp_mult. change (inj_Q IR ((q:Z_as_CRing)[^]n)) with (inj_Q_rh ((q:Z_as_CRing)[^]n)). rewrite <- rh_pres_mult. assert (inject_Z ((q:Z_as_CRing)[^]n) [=] (inject_Z (q:Z_as_CRing))[^]n). generalize n; clear; induction n; [reflexivity|]. rewrite <- nexp_Sn. rewrite <- nexp_Sn. rewrite <- IHn. reflexivity. rewrite -> H; clear H. set (H:=Q_Z_poly_apply P p q). cbv zeta in H. fold ZX_deg in H. fold n in H. rewrite -> H. apply Liouville_lemma4. intro. destruct (ap_imp_neq _ _ _ Hap); clear Hap. assert ((inject_Z (Zpos q))[^]n [#] [0]). generalize n; clear; induction n; [discriminate|]. intro; destruct IHn. rewrite <- nexp_Sn in H. destruct (Qmult_integral _ _ H); [discriminate|assumption]. rewrite -> H0 in H. apply (mult_eq_zero _ _ _ X); assumption. Qed.
imports: CRing_Homomorphisms CPoly_NthCoeff MoreFunctions Rolle Zlcm Q_can RX_deg QX_ZX QX_root_loc QX_extract_roots