proposition: Lemma Liouville_lemma8 : forall (n : nat) (q : positive), [1] [<=] (inj_Q_rh q)[^]n.
proof: Proof. intros n q; induction n. apply leEq_reflexive. rewrite <- nexp_Sn. apply (leEq_wdl _ ([1][*][1])); [|rational]. apply mult_resp_leEq_both; [apply less_leEq; apply pos_one|apply less_leEq; apply pos_one| |apply IHn]. rewrite <- (rh_pres_unit _ _ inj_Q_rh). apply inj_Q_leEq. simpl; unfold Qle; simpl; rewrite Pmult_1_r. unfold Z.le; simpl. case q; intros; discriminate. Qed.
imports: CRing_Homomorphisms CPoly_NthCoeff MoreFunctions Rolle Zlcm Q_can RX_deg QX_ZX QX_root_loc QX_extract_roots