proposition: Theorem Liouville_theorem2 : {n : nat | {C : IR | [0] [<] C | forall (x : Q), (C[*]inj_Q IR (1#Qden x)%Q[^]n) [<=] AbsIR (inj_Q _ x [-] a)}}.
proof: Proof. exists Liouville_degree. exists Liouville_constant. unfold Liouville_constant. apply recip_resp_pos. apply constant_pos. intro x. apply Liouville_theorem. Qed.
imports: CRing_Homomorphisms CPoly_NthCoeff MoreFunctions Rolle Zlcm Q_can RX_deg QX_ZX QX_root_loc QX_extract_roots