proposition: Lemma AbsIR_str_bnd : forall a b e : IR, AbsIR (a[-]b) [<] e -> b [<] a[+]e.
proof: Proof. intros. apply shift_less_plus'. apply leEq_less_trans with (AbsIR (a[-]b)); auto. eapply leEq_wdr; [ apply leEq_AbsIR | apply AbsIR_minus ]. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq