proposition: Lemma Abs_min_max : forall x, I x -> AbsIR x [<=] Max (AbsIR (left_end I I_fin)) (AbsIR (right_end I I_fin)).
proof: Proof. intros x HI; unfold left_end, right_end. destruct I; try inversion I_fin; destruct HI; apply abs_max; (apply less_leEq; assumption)|| assumption. Qed.
imports: CRing_Homomorphisms CPoly_NthCoeff MoreFunctions Rolle Zlcm Q_can RX_deg QX_ZX QX_root_loc QX_extract_roots