proposition: Lemma AbsIR_bnd_AbsIR : forall a b e, AbsIR (a[-]b) [<=] e -> AbsIR b [<=] AbsIR a[+]e.
proof: Proof. intros. apply shift_leEq_plus'. eapply leEq_transitive. apply triangle_IR_minus'. eapply leEq_wdl; [ apply H | apply AbsIR_minus ]. Qed.
imports: CoRN.reals.OddPolyRootIR