proposition: Lemma AbsIR_imp_AbsSmall : forall x y : IR, AbsIR x [<=] y -> AbsSmall y x.
proof: Proof. intros. unfold AbsSmall in |- *. simpl in H. unfold ABSIR in H. simpl in H. split. generalize (rht_leEq_Max x [--]x). intro H1. generalize (leEq_transitive _ _ (MAX x [--]x) _ H1 H). intro H2. rstepr ( [--][--]x). apply inv_resp_leEq. assumption. generalize (lft_leEq_Max x [--]x). intro H1. generalize (leEq_transitive _ _ (MAX x [--]x) _ H1 H). auto. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq