proposition: Lemma Liouville_lemma3 : forall x : IR, [1] [<] x or x [<] Two.
proof: Proof. intro x. apply less_cotransitive_unfolded. apply (less_wdl _ ([0][+][0][+][1])); [|rational]. apply plus_resp_less_rht. apply plus_resp_less_lft. apply pos_one. Qed.
imports: CRing_Homomorphisms CPoly_NthCoeff MoreFunctions Rolle Zlcm Q_can RX_deg QX_ZX QX_root_loc QX_extract_roots