proposition: Lemma AbsSmall_approach : forall (a b : IR), (forall (e : IR), [0][<]e -> AbsSmall (a[+]e) b) -> AbsSmall a b.
proof: Proof. unfold AbsSmall. intros a b H. split. assert (forall e : IR, [0][<]e -> [--]a[-]b[<=]e). intros. assert ([--](a[+]e)[<=]b /\ b[<=]a[+]e). apply H; auto. destruct H0. apply shift_minus_leEq. apply shift_leEq_plus'. astepl ([--]a[+][--]e). astepl ([--](a[+]e)). auto. astepr (b[+][0]). apply shift_leEq_plus'. apply approach_zero_weak; auto. assert (forall e : IR, [0][<]e -> b[-]a[<=]e). intros. assert ([--](a[+]e)[<=]b /\ b[<=]a[+]e). apply H; auto. destruct H0. apply shift_minus_leEq. astepr (a[+]e). auto. astepr (a[+][0]). apply shift_leEq_plus'. apply approach_zero_weak; auto. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq