proposition: Lemma a_in_Ia : Ia a.
proof: Proof. split. apply less_leEq. apply (less_wdr _ _ (a[-]([0][+][0][+][0]))); [|rational]. apply minus_resp_less_rht. apply plus_resp_less_both; [|apply pos_one]. apply plus_resp_less_lft; apply pos_one. apply less_leEq. apply (less_wdl _ (a[+]([0][+][0][+][0]))); [|rational]. apply plus_resp_less_lft. apply plus_resp_less_both; [|apply pos_one]. 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