proposition: Lemma abs_max : forall a b x, a [<=] x -> x [<=] b -> AbsIR x [<=] Max (AbsIR a) (AbsIR b).
proof: Proof. intros a b x Ha Hb. apply AbsIR_leEq. apply (leEq_transitive _ _ (AbsIR b)); [|apply rht_leEq_Max]. apply (leEq_transitive _ _ b); [assumption|apply leEq_AbsIR]. apply (leEq_transitive _ _ (AbsIR a)); [|apply lft_leEq_Max]. apply (leEq_transitive _ _ ([--]a)). apply inv_resp_leEq; assumption. rewrite -> AbsIR_inv; apply leEq_AbsIR. Qed.
imports: CRing_Homomorphisms CPoly_NthCoeff MoreFunctions Rolle Zlcm Q_can RX_deg QX_ZX QX_root_loc QX_extract_roots