proposition: Lemma AbsIR_leEq : forall a b, a [<=] b -> [--]a [<=] b -> AbsIR a [<=] b.
proof: Proof. intros a b Hp Hm. unfold AbsIR, ABSIR; simpl. apply Max_leEq; assumption. Qed.
imports: CRing_Homomorphisms CPoly_NthCoeff MoreFunctions Rolle Zlcm Q_can RX_deg QX_ZX QX_root_loc QX_extract_roots