proposition: Lemma AbsIR_str_bnd_AbsIR : forall a b e, AbsIR (a[-]b) [<] e -> AbsIR b [<] AbsIR a[+]e.
proof: Proof. do 3 intro. intro H. apply shift_less_plus'. eapply leEq_less_trans. apply triangle_IR_minus'. eapply less_wdl; [ apply H | apply AbsIR_minus ]. Qed.
imports: CoRN.reals.OddPolyRootIR