proposition: Lemma Liouville_lemma1 : forall x : IR, AbsIR (x[-]a) [<=] Two -> Ia x.
proof: Proof. intros x Hle. split. apply (leEq_wdr _ _ (x[+]Two[-]Two)); [|rational]. apply minus_resp_leEq. apply (leEq_wdl _ (x[+](a[-]x))); [|rational]. apply plus_resp_leEq_lft. rewrite -> AbsIR_minus in Hle. apply (leEq_transitive _ _ (AbsIR (a[-]x))); [|assumption]. apply leEq_AbsIR. apply (leEq_wdl _ (x[-]Two[+]Two)); [|rational]. apply plus_resp_leEq. apply (leEq_wdr _ _ (x[-](x[-]a))); [|rational]. apply minus_resp_leEq_rht. apply (leEq_transitive _ _ (AbsIR (x[-]a))); [|assumption]. apply leEq_AbsIR. Qed.
imports: CRing_Homomorphisms CPoly_NthCoeff MoreFunctions Rolle Zlcm Q_can RX_deg QX_ZX QX_root_loc QX_extract_roots