proposition: Theorem Liouville_theorem : forall (x : Q), (Liouville_constant[*]inj_Q IR (1#Qden x)%Q[^]Liouville_degree) [<=] AbsIR (inj_Q _ x [-] a).
proof: Proof. intro x. destruct x as [p q]; unfold Qden. apply (mult_cancel_leEq _ _ _ (inj_Q_rh q[^]Liouville_degree)). apply (less_leEq_trans _ _ [1]); [apply pos_one|]. apply Liouville_lemma8. assert (H : inj_Q IR (1#q)%Q = inj_Q_rh (1#q)%Q). reflexivity. rewrite H; clear H. rewrite <- nexp_ring_hom. rewrite <- CRings.mult_assoc. rewrite <- nexp_ring_hom. rewrite <- rh_pres_mult. assert (H : (1 # q)%Q[^]Liouville_degree[*](inject_Z q)[^]Liouville_degree [=] [1]). rewrite <- mult_nexp. rewrite <- (one_nexp _ Liouville_degree). apply nexp_wd; reflexivity. rewrite -> H; clear H. rewrite -> rh_pres_unit. rewrite -> mult_one. unfold Liouville_constant. apply shift_div_leEq'. apply constant_pos. assert (H : (inj_QX_rh (QX_extract_roots P)) ! a[=][0]). apply QX_extract_roots_spec_nrat; assumption. assert (H1 : (QX_extract_roots P) ! ((p # q)%Q)[#][0]). apply QX_extract_roots_spec_rat; assumption. apply (leEq_wdr _ _ _ _ (Liouville_lemma10 _ _ H _ _ H1)). fold C. rewrite -> (mult_commutes _ _ C). rewrite <- CRings.mult_assoc. apply mult_wdr. rewrite -> mult_commutes. apply mult_wdr. unfold Liouville_degree. symmetry; apply nexp_ring_hom. Qed.
imports: CRing_Homomorphisms CPoly_NthCoeff MoreFunctions Rolle Zlcm Q_can RX_deg QX_ZX QX_root_loc QX_extract_roots