proposition: Lemma Ia_proper : proper Ia.
proof: Proof. simpl. apply shift_minus_less. apply (less_wdl _ (a[+](([0][+][0][+][0])[+]([0][+][0][+][0])))); [|rational]. apply (less_wdr _ _ (a[+](Two[+]Two))); [|rational]. apply plus_resp_less_lft. apply plus_resp_less_both. apply plus_resp_less_both; [|apply pos_one]. apply plus_resp_less_lft; apply pos_one. 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