proposition: Lemma Liouville_lemma4 : forall p : Z_as_CRing, p [#] [0] -> [1] [<=] AbsIR (inj_Q_rh p).
proof: Proof. intros p Hap. change ([1][<=]AbsIR(inj_Q IR p)). rewrite -> AbsIR_Qabs. unfold Qabs.Qabs. unfold inject_Z. rewrite <- inj_Q_One. apply inj_Q_leEq. unfold Z.abs. destruct p. destruct Hap; reflexivity. simpl; unfold Qle; simpl; intuition. simpl; unfold Qle; simpl; intuition. Qed.
imports: CRing_Homomorphisms CPoly_NthCoeff MoreFunctions Rolle Zlcm Q_can RX_deg QX_ZX QX_root_loc QX_extract_roots